Verification oriented process ontology

N. O. Garanina ; I. S. Anureev ; O. I. Borovikova

Modelirovanie i analiz informacionnyh sistem, Tome 25 (2018) no. 6, pp. 607-622.

Résumé

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.

Détail

Keywords: ontology, verification, model checking
Mots-clés : concurrent processes.

Bibliographie

[1] Autili M. et al., “Aligning Qualitative, Real-Time, and Probabilistic Property Specification Patterns Using a Structured English Grammar”, IEEE Transactions on Software Engineering, 41:7 (2015), 620–638 | DOI

[2] Garanina N., Sidorova E., “Context-dependent Lexical and Syntactic Disambiguation in Ontology Population”, Concurrency, Specification and Programming (CS), Proc. of the 25th Int. Workshop (Humboldt-Universitat zu Berlin, 2016), 101–112

[3] Garanina N., Sidorova E., Bodin E., “A Multi-agent Text Analysis Based on Ontology of Subject Domain”, Perspectives of System Informatics (St. Petersburg, Russia, June 24–27), Lecture Notes in Computer Science, 8974, eds. Voronkov A., Virbitskaite I., Springer, Berlin–Heidelberg, 2015, 102–110 | DOI | MR | Zbl

[4] Garanina N. et al., “Using Multiple Semantic Measures For Coreference Resolution In Ontology Population”, International Journal of Computing, 16:3 (2017), 166–176

[5] Garanina N., Zyubin V., Liakh T., “Ontological Approach to Organizing Specification Patterns in the Framework of Support System for Formal Verification of Distributed Program Systems”, System Informatics, 9 (2017), 111–132 | DOI

[6] Hepp M., Dumitru R., “An Ontology Framework for Semantic Business Process Management”, Wirtschaftsinformatik Proc. (Karlsruhe, Germany, February 28 – March 2, 2007), 423–440 https://aisel.aisnet.org/wi2007/27/

[7] Hepp M. et al., “Semantic Business Process Management: A Vision Towards Using Semantic Web Services for Business Process Management”, e-Business Engineering, Proc. Int. Conf. ICEBE 2005 (Beijing, China, October 12–18, 2005), IEEE, 535–540 | DOI

[8] HermiT OWL Reasoner, http://www.hermit-reasoner.com/

[9] Herre H., “General Formal Ontology (GFO): A Foundational Ontology for Conceptual Modelling”, Theory and Applications of Ontology: Computer Applications, eds. Poli R., Healy M., Kameas A., Springer, Dordrecht, 2010, 297–345 | DOI

[10] Hoare C. A. R., Communicating sequential processes, Prentice-Hall, 1985, 256 pp. | MR | Zbl

[11] Holzmann G. J., The Spin Model Checker: Primer and Reference Manual, Addison-Wesley Professional, 2003, 608 pp.

[12] Horrocks I. et al., SWRL: A Semantic Web Rule Language combining OWL and RuleML, http://www.w3.org/Submission/SWRL

[13] D.L. McGuinness, F. Harmelen van (eds.), OWL Web Ontology Language Overview: W3C Recommendation, , 10 February 2004 https://www.w3.org/TR/owl-features/

[14] Protégé. A free, open-source ontology editor and framework for building intelligent systems, http://protege.stanford.edu/

[15] Salamah S., Gates A.Q., Kreinovich V., “Validated patterns for specification of complex LTL formulas”, Journal of Systems and Software, 85:8 (2012), 1915–1929 | DOI

[16] Schlenoff C. et al., The Process Specification Language (PSL): Overview and Version 1.0 Specification, NIST Interagency/Internal Report (NISTIR), No 6459, 1999 https://www.nist.gov/publications/process-specification-language-psl-overview-and-version-10-specification

[17] Shanmugham S. G., Roberts C. A., “Application of graphical specification methodologies to manufacturing control logic development: A classification and comparison”, International Journal of Computer Integrated Manufacturing, 11:2 (1998), 142–152 | DOI

[18] Stuart A., Curtis J., “A Process Ontology”, Knowledge Engineering and Knowledge Management: Ontologies and the Semantic Web, Proc. of the 13th Int. Conference EKAW 2002 (Sigüenza, Spain, October 01–04, 2002), Lecture Notes in Computer Science, 2473, eds. Gómez-Pérez A., Benjamins V. R., Springer, Berlin–Heidelberg, 108–113 | DOI | Zbl

[19] Wong P. Y. H., Gibbons J., “Property Specifications for Workflow Modelling”, Integrated Formal Methods, Proc. Int. Conf. IFM 2009 (Düsseldorf, Germany, February 16–19, 2009), Lecture Notes in Computer Science, 5423, eds. Leuschel M., Wehrheim H., Springer, Berlin–Heidelberg, 166–180 | DOI

[20] Yu J. et al., “Pattern based property specification and verification for service composition”, Web Information Systems, Proc. of 7th Int. Conf. WISE 2006 (Wuhan, China, October 23–26, 2006), Lecture Notes in Computer Science, 4255, eds. Aberer K. et al., Springer, Berlin–Heidelberg, 156–168 | DOI