Methods for Domain Specification of Verification-Oriented Process Ontology
User-friendly formal specifications and verification of parallel and distributed systems from various subject fields, such as automatic control, telecommunications, business processes, are active research topics due to its practical significance. In this paper, we present methods for the development...
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2019-12-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/1275 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1850024003553460224 |
|---|---|
| author | Natalia O. Garanina Igor S. Anureev Olesya I. Borovikova Vladimir E. Zyubin |
| author_facet | Natalia O. Garanina Igor S. Anureev Olesya I. Borovikova Vladimir E. Zyubin |
| author_sort | Natalia O. Garanina |
| collection | DOAJ |
| description | User-friendly formal specifications and verification of parallel and distributed systems from various subject fields, such as automatic control, telecommunications, business processes, are active research topics due to its practical significance. In this paper, we present methods for the development of verification-oriented domain-specific process ontologies which are used to describe parallel and distributed systems of subject fields. One of the advantages of such ontologies is their formal semantics which make possible formal verification of the described systems. Our method is based on the abstract verification-oriented process ontology. We use two methods of specialization of the abstract process ontology. The declarative method uses the specialization of the classes of the original ontology, introduction of new declarative classes, as well as use of new axioms system, which restrict the classes and relations of the abstract ontology. The constructive method uses semantic markup and pattern matching techniques to link sublect fields with classes of the abstract process ontology. We provide detailed ontological specifications for these techniques. Our methods preserve the formal semantics of the original process ontology and, therefore, the possibility of applying formal verification methods to the specialized process ontologies. We show that the constructive method is a refinement of the declarative method. The construction of ontology of the typical elements of automatic control systems illustrates our methods: we develop a declarative description of the classes and restrictions for the specialized ontology in the Prot´eg´e system in the OWL language using the deriving rules written in the SWRL language and we construct the system of semantic markup templates which implements typical elements of automatic control systems. |
| format | Article |
| id | doaj-art-d95a31ebc0cb454cbea21c5360f79092 |
| institution | DOAJ |
| issn | 1818-1015 2313-5417 |
| language | English |
| publishDate | 2019-12-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj-art-d95a31ebc0cb454cbea21c5360f790922025-08-20T03:01:14ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172019-12-0126453454910.18255/1818-1015-2019-4-534-549952Methods for Domain Specification of Verification-Oriented Process OntologyNatalia O. Garanina0Igor S. Anureev1Olesya I. Borovikova2Vladimir E. Zyubin3A.P. Ershov Institute of Informatics Systems SB RAS, Institute of Automation and Electrometry SB RASA.P. Ershov Institute of Informatics Systems SB RAS, Institute of Automation and Electrometry SB RASA.P. Ershov Institute of Informatics Systems SB RASInstitute of Automation and Electrometry SB RASUser-friendly formal specifications and verification of parallel and distributed systems from various subject fields, such as automatic control, telecommunications, business processes, are active research topics due to its practical significance. In this paper, we present methods for the development of verification-oriented domain-specific process ontologies which are used to describe parallel and distributed systems of subject fields. One of the advantages of such ontologies is their formal semantics which make possible formal verification of the described systems. Our method is based on the abstract verification-oriented process ontology. We use two methods of specialization of the abstract process ontology. The declarative method uses the specialization of the classes of the original ontology, introduction of new declarative classes, as well as use of new axioms system, which restrict the classes and relations of the abstract ontology. The constructive method uses semantic markup and pattern matching techniques to link sublect fields with classes of the abstract process ontology. We provide detailed ontological specifications for these techniques. Our methods preserve the formal semantics of the original process ontology and, therefore, the possibility of applying formal verification methods to the specialized process ontologies. We show that the constructive method is a refinement of the declarative method. The construction of ontology of the typical elements of automatic control systems illustrates our methods: we develop a declarative description of the classes and restrictions for the specialized ontology in the Prot´eg´e system in the OWL language using the deriving rules written in the SWRL language and we construct the system of semantic markup templates which implements typical elements of automatic control systems.https://www.mais-journal.ru/jour/article/view/1275process ontologyspecializationontology axiomspattern matchingsemantic markupautomatic control systemformal verification |
| spellingShingle | Natalia O. Garanina Igor S. Anureev Olesya I. Borovikova Vladimir E. Zyubin Methods for Domain Specification of Verification-Oriented Process Ontology Моделирование и анализ информационных систем process ontology specialization ontology axioms pattern matching semantic markup automatic control system formal verification |
| title | Methods for Domain Specification of Verification-Oriented Process Ontology |
| title_full | Methods for Domain Specification of Verification-Oriented Process Ontology |
| title_fullStr | Methods for Domain Specification of Verification-Oriented Process Ontology |
| title_full_unstemmed | Methods for Domain Specification of Verification-Oriented Process Ontology |
| title_short | Methods for Domain Specification of Verification-Oriented Process Ontology |
| title_sort | methods for domain specification of verification oriented process ontology |
| topic | process ontology specialization ontology axioms pattern matching semantic markup automatic control system formal verification |
| url | https://www.mais-journal.ru/jour/article/view/1275 |
| work_keys_str_mv | AT nataliaogaranina methodsfordomainspecificationofverificationorientedprocessontology AT igorsanureev methodsfordomainspecificationofverificationorientedprocessontology AT olesyaiborovikova methodsfordomainspecificationofverificationorientedprocessontology AT vladimirezyubin methodsfordomainspecificationofverificationorientedprocessontology |