Verification Oriented Process Ontology
https://doi.org/10.18255/1818-1015-2018-6-607-622
Abstract
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 ́eg ́e in 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.
About the Authors
Natalia O. Garanina
A.P. Ershov Institute of Informatics Systems
Russian Federation
Russian Federation
PhD, senior researcher
6 Acad. Lavrentjev pr., Novosibirsk 630060
Igor S. Anureev
A.P. Ershov Institute of Informatics Systems
Russian Federation
Russian Federation
PhD, senior researcher
6 Acad. Lavrentjev pr., Novosibirsk 630060
Olesya I. Borovikova
A.P. Ershov Institute of Informatics Systems
Russian Federation
Russian Federation
junior researcher
6 Acad. Lavrentjev pr., Novosibirsk 630060
References
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, https://doi.org/10.1109/TSE.2015.2398877.
2. Garanina N., Sidorova E., “Context-dependent Lexical and Syntactic Disambiguation in Ontology Population”, Concurrency, Specification and Programming (CS&P), 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. PSI 2014, Proc. Int. Conference (St. Petersburg, Russia, June 24–27), Lecture Notes in Computer Science, 8974, eds. Voronkov A., Virbitskaite I., Springer, Berlin, Heidelberg, 2015, 102–110, https: //doi.org/10.1007/978-3-662-46823-4_9.
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, http://dx.doi.org/10. 31144/si.2307-6410.2017.n9.p111-132.
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 (ICEBE 2005), Proc. Int. Conf. (Beijing, China, October 12–18), IEEE, 2005, 535–540, https://doi.org/10.1109/ICEBE.2005.110.
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, https://doi.org/10.1007/ 978-90-481-8847-5_14.
10. Hoare C.A.R., Communicating sequential processes, Prentice-Hall, 1985, 256 pp.
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. OWL Web Ontology Language Overview: W3C Recommendation 10 February 2004, https://www.w3.org/TR/owl-features/, eds. D.L. McGuinness, F. Harmelen van..
14. Prot ́eg ́e. 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, https://doi. org/10.1016/j.jss.2012.02.041.
16. Schlenoff C. et al., The Process Specification Language (PSL): Overview and Version 1.0 Specification, NIST Interagency/Internal Report (NISTIR), 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, http://dx.doi. org/10.1080/095119298130886.
18. Stuart A., Curtis J., “A Process Ontology”, Knowledge Engineering and Knowledge Management: Ontologies and the Semantic Web. EKAW 2002, Proc. of the 13th Int. Conference (Sigu ̈enza, Spain, October 01–04), Lecture Notes in Computer Science, 2473, eds. G ́omez-P ́erez A., Benjamins V.R., Springer, Berlin, Heidelberg, 2002, 108–113, https://doi.org/10.1007/3-540-45810-7_13.
19. Wong P.Y.H., Gibbons J., “Property Specifications for Workflow Modelling”, Integrated Formal Methods. IFM 2009, Proc. Int. Conf. (Du ̈sseldorf, Germany, February 16–19), Lecture Notes in Computer Science, 5423, eds. Leuschel M., Wehrheim H., Springer, Berlin, Heidelberg, 2009, 166–180, https://doi.org/10.1007/978-3-642-00255-7_5.
20. Yu J.et al.,“Pattern based property specification and verification for service composition”, Web Information Systems. WISE 2006, Proc. of 7th Int. Conf. (Wuhan, China, October 23–26), Lecture Notes in Computer Science, 4255, eds. Aberer K. et al., Springer, Berlin, Heidelberg, 2006, 156–168, https://doi.org/10.1007/11912873_18.
Review
For citations:
Garanina N.O., Anureev I.S., Borovikova O.I. Verification Oriented Process Ontology. Modeling and Analysis of Information Systems. 2018;25(6):607-622. (In Russ.) https://doi.org/10.18255/1818-1015-2018-6-607-622
Views:
860
Email this article 