User-friendly formal specification and verification of concurrent and distributed systems for various domains, such as automatic control systems, telecommunications, and business processes, are active research topics due to their practical significance. In this paper, we present methods of developing verification-oriented domain-specific process ontologies used to describe concurrent systems of subject domains. One of the advantages of such ontologies is their formal semantics, which provides formal verification of the described systems. Our method is based on an abstract verification-oriented process ontology. We use two methods of domain specialization of the abstract process ontology. The declarative method relies on specializing classes of the original ontology, introducing new declarative classes, and using a new set of axioms to set restrictions on classes and relations of the abstract ontology. The constructive method uses semantic markup and pattern matching techniques to link domain concepts to 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; therefore, formal verification methods can be applied to the resulting domain-specific process ontologies. We demonstrate that the constructive method is a refined version of the declarative method. We illustrate our methods on the example of constructing an ontology for standard elements of automatic control systems: we develop declarative descriptions of the classes and restrictions of the domain-specific ontology in the Protégé system in the Web Ontology Language (OWL) using inference rules written in the Semantic Web Rule Language (SWRL) and construct a system of semantic markup patterns that implements standard elements of automatic control systems.
This is a preview of subscription content, access via your institution.
Buy single article
Instant access to the full article PDF.
Tax calculation will be finalised during checkout.
Börger, E. and Stärk, R., Abstract State Machines: A Method for High-Level System Design and Analysis, Springer-Verlag, 2003.
Gangemi, A. and Presutti, V., Ontology design patterns, in Handbook on Ontologies, Springer, 2009, 2nd ed., pp. 221–243.
Garanina, N.O., Zubin, V., Lyakh, T., and 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, 2018, vol. 303, pp. 515–528.
Garanina, N. and Anureev, I., Verification oriented process ontology, Proceedings of the 9th Workshop Program Semantics, Specification and Verification: Theory and Applications, PSSV 2018, 2018, pp. 58–67.
Garanina, N., Sidorova, E., and Bodin, E., A multi-agent text analysis based on ontology of subject domain, Lect. Notes Comput. Sci., 2015, vol. 8974, pp. 102–110.
Clarke, E.M., Henzinger, Th.A., Veith, H., and Bloem, R., Handbook of Model Checking, Springer, 2018, vol. 10.
Staab, S. and Studer, R., Handbook on Ontologies, Springer Science & Business Media, 2010.
Scherp, A., Saathoff, C., Franz, T., and Staab, S., Designing core ontologies, Appl. Ontol., 2011, vol. 6, no. 3, pp. 177–221.
HermiT OWL Reasoner. https://www.hermit-reasoner.com. Accessed September 29, 2019.
Ontology Design Patterns. https://www.ontologydesignpatterns.org. Accessed September 29, 2019.
OWL Web Ontology Language Overview: W3C Recommendation 10 February 2004. https://w3.org/TR/owl-features/. Accessed September 29, 2019.
Protégé. A Free, Open-Source Ontology Editor and Framework for Building Intelligent Systems. https://protege.stanford.edu/. Accessed September 29, 2019.
Horrocks, I., et al., SWRL: A Semantic Web Rule Language Combining OWL and RuleML. https://www.w3.org/ Submission/SWRL. Accessed September 29, 2019.
The study was supported by the Russian Foundation for Basic Research, projects no. 17-07-01600 and no. 19-07-00762 and the Russian Ministry of Education and Science, project no. AAAA-A19-119120290056-0.
CONFLICT OF INTEREST
The authors declare that they have no conflicts of interest.
Natalia O. Garanina, orcid.org/0000-0001-9734-3808, PhD, senior researcher.
Igor S. Anureev, orcid.org/0000-0001-9574-128X, PhD, senior researcher.
Olesya I. Borovikova, orcid.org/0000-0001-5456-8513, junior researcher.
Vladimir E. Zyubin, orcid.org/0000-0002-8198-3197, DSci, head of laboratory.
Translated by A. Ovchinnikova
About this article
Cite this article
Garanina, N.O., Anureev, I.S., Borovikova, O.I. et al. Methods for Domain Specialization of Verification-Oriented Process Ontologies. Aut. Control Comp. Sci. 54, 740–751 (2020). https://doi.org/10.3103/S014641162007007X
- process ontology
- domain specification
- ontology axioms
- pattern matching
- semantic markup
- automatic control system
- formal verification