Geodesic
Methods for domain specification of verification-oriented process ontology
Modelirovanie i analiz informacionnyh sistem, Tome 26 (2019) no. 4, pp. 534-549

Voir la notice de l'article provenant de la source Math-Net.Ru

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égé 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.
Keywords: process ontology, specialization, ontology axioms, pattern matching, semantic markup, automatic control system, formal verification. 
@article{MAIS_2019_26_4_a5,
     author = {N. O. Garanina and I. S. Anureev and O. I. Borovikova and V. E. Zyubin},
     title = {Methods for domain specification of verification-oriented process ontology},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {534--549},
     publisher = {mathdoc},
     volume = {26},
     number = {4},
     year = {2019},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2019_26_4_a5/}
}
TY  - JOUR
AU  - N. O. Garanina
AU  - I. S. Anureev
AU  - O. I. Borovikova
AU  - V. E. Zyubin
TI  - Methods for domain specification of verification-oriented process ontology
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2019
SP  - 534
EP  - 549
VL  - 26
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2019_26_4_a5/
LA  - ru
ID  - MAIS_2019_26_4_a5
ER  - 
%0 Journal Article
%A N. O. Garanina
%A I. S. Anureev
%A O. I. Borovikova
%A V. E. Zyubin
%T Methods for domain specification of verification-oriented process ontology
%J Modelirovanie i analiz informacionnyh sistem
%D 2019
%P 534-549
%V 26
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2019_26_4_a5/
%G ru
%F MAIS_2019_26_4_a5
N. O. Garanina; I. S. Anureev; O. I. Borovikova; V. E. Zyubin. Methods for domain specification of verification-oriented process ontology. Modelirovanie i analiz informacionnyh sistem, Tome 26 (2019) no. 4, pp. 534-549. http://geodesic.mathdoc.fr/item/MAIS_2019_26_4_a5/