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 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.

process ontology, specialization, ontology axioms, pattern matching, semantic markup, automatic control system, formal verification

1. Borger E., St¨ark R., Abstract State Machines: A Method for High-Level System Design and Analysis, Springer-Verlag, 2003.

2. Gangemi A., Presutti V., “Ontology Design Patterns”, Handbook on Ontologies, Springer, Second Edition, 2009, 221–243.

3. Garanina N. O., Zubin V., Lyakh T., Gorlatch S., “An Ontology of Specification Patterns for Verification of Concurrent Systems”, Proceedings of the 17th International Conference SoMeT-18, New Trends in Intelligent Software Methodologies, Tools and Techniques, Series: Frontiers in Artificial Intelligence and Applications, 303 (2018), 515-528.

4. Garanina N., Anureev I., “Verification Oriented Process Ontology”, Proceedings of the 9th Workshop “Program Semantics, Specification and Verification: Theory and Applications”, PSSV 2018, 2018, 58–67.

5. Garanina N., Sidorova E., Bodin E., “A Multi-agent Text Analysis Based on Ontology of Subject Domain”, Perspectives of System Informatics. PSI 2014. Lecture Notes in Computer Science, 8974 (2015), 102–110.

6. Clarke E. M., Henzinger Th. A., Veith H., Bloem R., Handbook of Model Checking, 10, Springer, 2018.

7. Staab S., Studer R., Handbook on Ontologies, Springer Science & Business Media, 2010.

8. Scherp. A., Saathoff C., Franz T., Staab S, “Designing Core Ontologies”, Applied Ontology, IOS Press, 6:3 (2011), 177–221.

9. HermiT OWL Reasoner, www.hermit-reasoner.com, (29.09.2019).

10. Ontology design patterns, www.ontologydesignpatterns.org, (29.09.2019).

11. OWL Web Ontology Language Overview: W3C Recommendation 10 February 2004, www.w3.org/TR/owl-features/, (29.09.2019).

12. Prot´eg´e. A Free, Open-source Ontology Editor and Framework for Building Intelligent Systems, protege.stanford.edu, (29.09.2019).

13. Horrocks I. et al., “SWRL: A Semantic Web Rule Language Combining OWL and RuleML”, www.w3.org/Submission/SWRL, (29.09.2019).