maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2018-6-607-622mais-762Research ArticleОригинальные статьиArticlesОнтология процессов, ориентированная на верификациюVerification Oriented Process Ontologyhttps://orcid.org/0000-0001-9734-3808ГаранинаНаталья ОлеговнаGaraninaNatalia O.

канд. физ.-мат. наук, ст. науч. сотр.

пр. акад. Лаврентьева, 6, г. Новосибирск, 630090

PhD, senior researcher

6 Acad. Lavrentjev pr., Novosibirsk 630060

garanina@iis.nsk.suhttps://orcid.org/0000-0001-9574-128XАнуреевИгорь СергеевичAnureevIgor S.

канд. физ.-мат. наук, ст. науч. сотр.

пр. акад. Лаврентьева, 6, г. Новосибирск, 630090

PhD, senior researcher

6 Acad. Lavrentjev pr., Novosibirsk 630060

anureev@iis.nsk.suhttps://orcid.org/0000-0001-5456-8513БоровиковаОлеся ИгнатьевнаBorovikovaOlesya I.

мл. науч. сотр.

пр. акад. Лаврентьева, 6, г. Новосибирск, 630090

junior researcher

6 Acad. Lavrentjev pr., Novosibirsk 630060

olesya@iis.nsk.suИнститут систем информатики имени А.П. Ершова СО РАНРоссияA.P. Ershov Institute of Informatics SystemsRussian Federation201819122018256607622Copyright © Гаранина Н.О., Ануреев И.С., Боровикова О.И., 20182018Гаранина Н.О., Ануреев И.С., Боровикова О.И.Garanina N.O., Anureev I.S., Borovikova O.I.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/762

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

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.

онтологияверификацияпроверка моделейпроцессыontologyverificationmodel checkingconcurrent processesРабота поддержана грантом РФФИ 17-07-01600ReferencesAutili 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.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.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.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.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.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.Garanina N. et al., “Using Multiple Semantic Measures For Coreference Resolution In Ontology Population”, International Journal of Computing, 16:3 (2017), 166–176.Garanina N. et al., “Using Multiple Semantic Measures For Coreference Resolution In Ontology Population”, International Journal of Computing, 16:3 (2017), 166–176.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.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.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/.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/.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.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.HermiT OWL Reasoner, http://www.hermit-reasoner.com/.HermiT OWL Reasoner, http://www.hermit-reasoner.com/.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.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.Hoare C.A.R., Communicating sequential processes, Prentice-Hall, 1985, 256 pp.Hoare C.A.R., Communicating sequential processes, Prentice-Hall, 1985, 256 pp.Holzmann G.J., The Spin Model Checker: Primer and Reference Manual, Addison-Wesley Professional, 2003, 608 pp.Holzmann G.J., The Spin Model Checker: Primer and Reference Manual, Addison-Wesley Professional, 2003, 608 pp.Horrocks I. et al., SWRL: A Semantic Web Rule Language combining OWL and RuleML, http://www.w3.org/Submission/SWRL.Horrocks I. et al., SWRL: A Semantic Web Rule Language combining OWL and RuleML, http://www.w3.org/Submission/SWRL.OWL Web Ontology Language Overview: W3C Recommendation 10 February 2004, https://www.w3.org/TR/owl-features/, eds. D.L. McGuinness, F. Harmelen van..OWL Web Ontology Language Overview: W3C Recommendation 10 February 2004, https://www.w3.org/TR/owl-features/, eds. D.L. McGuinness, F. Harmelen van..Prot ́eg ́e. A free, open-source ontology editor and framework for building intelligent systems, http://protege.stanford.edu/.Prot ́eg ́e. A free, open-source ontology editor and framework for building intelligent systems, http://protege.stanford.edu/.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.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.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.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.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.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.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.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.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.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.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.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.

The authors declare that there are no conflicts of interest present.