Онтология процессов, ориентированная на верификацию

В статье представлена онтология процессов, близких взаимодействующим последовательным процессам Хоара. Она является частью интеллектуальной системы поддержки верификации свойств поведения таких процессов. Наше онтологическое представление процессов ориентировано как на применение формальных методов верификации, так и на извлечение информации из технической документации (с помощью нашей ранее разработанной системы извлечения информации из текстов на естественном языке). Мы описываем классы и домены онтологии, которые определяют взаимодействующие процессы. Эти процессы характеризуются множествами локальных и разделяемых переменных, списком действий над этими переменными, которые изменяют их значения, списком каналов взаимодействия процессов (которые, в свою очередь, характеризуются типом чтения сообщений, емкостью, способами записи и считывания, а также надежностью), списком коммуникационных действий для отправки сообщений. Помимо формального математического определения классов и доменов онтологии, приведены примеры описаний некоторых онтологических классов, а также типовых свойств и аксиом для них в редакторе Prot ́eg ́e на языке OWL с использованием правил вывода на языке SWRL. Для онтологического представления взаимодействующих процессов определяется их формальная операционная семантика, которая задается с использованием помеченной системы переходов. В интерливинговой модели она сводится к локальной операционной семантике отдельных экземпляров процессов. Представлена специализация онтологии для некоторых типов процессов из предметной области систем автоматического управления, моделирующих типовые функциональные элементы системы автоматического управления (датчики, сравнивающие устройства и регулирующие устройства), а также их комбинации. Понятия специализированной онтологии иллюстрируются на примере управляющей части системы розлива бутылок.

онтология, верификация, проверка моделей, процессы

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.