Geodesic
Verification oriented process ontology
Modelirovanie i analiz informacionnyh sistem, Tome 25 (2018) no. 6, pp. 607-622

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

This paper presents the ontology of the concurrent processes close to Hoare communicating sequential processes. It is the part of the intellectual system for supporting verification of behavioural properties of these processes. Our ontological representation of the processes is oriented both to the application of formal verification methods and to the extraction of information from technical documentation (by our previously developed system of information extraction from a natural language text). We describe the ontology classes and domains that define communicating concurrent processes. These processes are characterized by sets of local and shared variables, a list of actions on these variables which change their values, a list of channels for the process communication (which, in turn, are characterized by the type of reading messages, capacity, ways of writing and reading, and reliability), and also a list of communication actions for sending messages. In addition to the formal mathematical definition of classes and domains of the ontology, examples of descriptions of some ontological classes as well as typical properties and axioms for them are specified in the editor Protǵín the OWL language with the use of the inference rules in the SWRL language. The formal operational semantics of communicating processes is determined on their ontological representation and is given as a labelled transition system. It is reduced to the local operational semantics of separate process instances in the interleaving model. We specialize several types of processes from the subject domain of automatic control systems that model the typical functional elements of the automatic control system (sensors, comparators and regulators) as well as their combinations. The concepts of the specialized ontology are illustrated by the example of a control part for a bottle-filling system.
Keywords: ontology, verification, model checking
Mots-clés : concurrent processes. 
@article{MAIS_2018_25_6_a1,
     author = {N. O. Garanina and I. S. Anureev and O. I. Borovikova},
     title = {Verification oriented process ontology},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {607--622},
     publisher = {mathdoc},
     volume = {25},
     number = {6},
     year = {2018},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2018_25_6_a1/}
}
TY  - JOUR
AU  - N. O. Garanina
AU  - I. S. Anureev
AU  - O. I. Borovikova
TI  - Verification oriented process ontology
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2018
SP  - 607
EP  - 622
VL  - 25
IS  - 6
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2018_25_6_a1/
LA  - ru
ID  - MAIS_2018_25_6_a1
ER  - 
%0 Journal Article
%A N. O. Garanina
%A I. S. Anureev
%A O. I. Borovikova
%T Verification oriented process ontology
%J Modelirovanie i analiz informacionnyh sistem
%D 2018
%P 607-622
%V 25
%N 6
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2018_25_6_a1/
%G ru
%F MAIS_2018_25_6_a1
N. O. Garanina; I. S. Anureev; O. I. Borovikova. Verification oriented process ontology. Modelirovanie i analiz informacionnyh sistem, Tome 25 (2018) no. 6, pp. 607-622. http://geodesic.mathdoc.fr/item/MAIS_2018_25_6_a1/