Методы специализации онтологии процессов, ориентированной на верификацию

Удобная для пользователя формальная спецификация и верификация параллельных и распределённых систем, принадлежащих различным предметным областям, таким как системы автоматического управления, телекоммуникации, бизнес-процессы, являются активными темами исследований в силу их практической значимости. В этой статье мы представляем методы разработки специализированных ориентированных на верификацию онтологий процессов, которые используются для описания параллельных и распределенных систем предметных областей. Одним из преимуществ таких онтологий является их формальная семантика, которая делает возможной формальную верификацию описанных систем. Наш метод основан на абстрактной онтологии процессов, ориентированной на верификацию. Мы используем два метода специализации абстрактной онтологии процессов. Декларативный метод с помощью специализации классов исходной онтологии, введения новых декларативных классов, а также системы аксиом задаёт ограничения для классов и отношений абстрактной онтологии. Конструктивный метод использует техники семантической разметки и сопоставления с образцом, чтобы связать понятия предметной области с классами абстрактной онтологии процессов. Мы даём подробные онтологические спецификации этих техник. Наши методы сохраняют формальную семантику исходной онтологии процессов и, следовательно, возможность применения формальных методов верификации к специализированным онтологиям процессов. Мы показываем, что конструктивный метод является уточнением декларативного метода. Построение онтологии типовых элементов систем автоматического управления иллюстрирует наши методы: разработано декларативное описание классов и ограничений специализированной онтологии в системе Protege на языке OWL с использованием правил вывода на языке SWRL и построена система шаблонов семантической разметки, которая реализует типовые элементы систем автоматического управления.

онтология процессов, специализация, аксиомы онтологии, сопоставление с образцом, семантическая разметка, системы автоматического управления, верификация

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