ntvНаучно-технический вестник информационных технологий, механики и оптикиScientific and Technical Journal of Information Technologies, Mechanics and Optics2226-14942500-0373Университет ИТМО10.17586/2226-1494-2023-23-4-750-756ntv-206Research ArticleКОМПЬЮТЕРНЫЕ СИСТЕМЫ И ИНФОРМАЦИОННЫЕ ТЕХНОЛОГИИCOMPUTER SCIENCEВерификация событийно-управляемых программных систем с использованием языка спецификации взаимодействующих автоматных объектовVerifcation of event-driven software systems using the specifcation language of cooperating automata objectshttps://orcid.org/0000-0003-4225-4124АфанасьеваИ. В.AfanasievaI. V.

Афанасьева Ирина Викторовна — кандидат технических наук, заведующий лабораторией

sc 57210431774

Нижний Архыз, 369167

Irina V. Afanasieva — PhD, Head of Laboratory

sc 57210431774

Nizhny Arkhyz, 369167

riv615@gmail.comhttps://orcid.org/0000-0003-4450-0173НовиковФ. А.NovikovF. A.

Новиков Федор Александрович — доктор технических наук, старший научный сотрудник, профессор; профессор

sc 16441904500

Санкт-Петербург, 195251

Санкт-Петербург, 194021

Fedor A. Novikov — D.Sc., Senior Researcher, Professor; Professor

sc 16441904500

Saint Petersburg, 195251

Saint Peterburg, 194021

fedornovikov51@gmail.comhttps://orcid.org/0000-0002-4008-9316ФедорченкоЛ. Н.FedorchenkoL. N.

Федорченко Людмила Николаевна — кандидат технических наук, старший научный сотрудник

sc 36561350100

Санкт-Петербург, 199178

Ludmila N. Fedorchenko — PhD, Senior Researcher

sc 36561350100

Saint Petersburg, 199178

lnf@iias.spb.suСпециальная астрофизическая обсерватория Российской академии наукРоссияSpecial Astrophysical Observatory of the Russian Academy of Sciences (SAO RAS)Russian FederationСанкт-Петербургский политехнический университет Петра Великого; Санкт-Петербургский национальный исследовательский Академический университет имени Ж.И. Алфёрова Российской академии наукРоссияPeter the Great St. Petersburg Polytechnic University (SPbPU); Alferov Academic UniversityRussian FederationСанкт-Петербургский Федеральный исследовательский центр Российской академии наукРоссияSt. Petersburg Federal Research Center of the Russian Academy of SciencesRussian Federation202314122024234750756Copyright © Афанасьева И.В., Новиков Ф.А., Федорченко Л.Н., 20242024Афанасьева И.В., Новиков Ф.А., Федорченко Л.Н.Afanasieva I.V., Novikov F.A., Fedorchenko L.N.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://ntv.elpub.ru/jour/article/view/206

Введение. Язык спецификации Cooperative Interaction Automata Objects (CIAO) предназначен для описания поведения распределенных и параллельных систем, управляемых событиями. К этому классу систем относятся различные программно-аппаратные комплексы управления, контроля, сбора и обработки данных. Возможность автоматической проверки соответствия требованиям является желательным конкурентным преимуществом событийно-управляемых программных систем. Язык CIAO расширяет концепцию конечных автоматов (Unifed Modeling Language, UML) возможностью кооперативного взаимодействия нескольких автоматов через строго определенные интерфейсы. Кооперативное взаимодействие автоматных объектов определяется схемой связи, которая связывает предоставленные и требуемые интерфейсы различных автоматных объектов. Таким образом, поведение системы в целом можно описать как набор протоколов выполнения, каждый из которых представляет собой последовательность вызовов интерфейса, возможно со сторожевыми условиями. Метод. Представлен набор протоколов с помощью семантического графа, в котором все возможные пути от начальных к конечным узлам определены последовательностью вызовов методов интерфейса. Благодаря тому, что интерфейсы заранее строго определены схемой связи, возможно автоматическое построение семантического графа по заданной системе взаимодействующих автоматных объектов. Для проверки поведения системы достаточно убедиться, что каждый путь в семантическом графе удовлетворяет требованиям. Системные требования формально описаны с помощью условных регулярных выражений, определяющих шаблоны допустимого и запрещенного поведения. Основные результаты. Предложены методы и алгоритмы, позволяющие автоматически проверить соответствие программ на языке CIAO заданным требованиям. Обсуждение. Разработанный метод сужает формализм для задания спецификаций до класса регулярных языков, а язык программирования — до языка с простой и предопределенной структурой. Во многих практических случаях этого достаточно для эффективной верификации.

The CIAO (Cooperative Interaction Automata Objects) specifcation language is intended to describe the behavior of distributed and parallel event-driven systems. This class of systems includes various software and hardware systems for control, monitoring, data collection, and processing. The ability to verify compliance with requirements is desirable competitive advantage for such systems. The CIAO language extends the concept of state machines of the UML (Unifed Modeling Language) with the possibility of cooperative interaction of several automata through strictly defned interfaces. The cooperative interaction of automatа objects is defned by a link scheme that defnes how the provided and required interfaces of different automatа objects are connected. Thus, the behavior of the system as a whole could be described as a set of execution protocols, each of which is a sequence of interface calls, possibly with guard conditions. We represent a set of protocols using a semantic graph in which all possible paths from the initial nodes to the fnal nodes defne sequences of interface method calls. Because the interfaces are strictly defned in advance by the connection scheme, it is possible to construct a semantic graph automatically according to a given system of interacting automaton objects. To verify the system behavior, one only has to check if each path in the semantic graph does satisfy the requirements. System requirements are formally described using conditional regular expressions that defne patterns of acceptable and forbidden behavior. This article proposes methods and algorithms that allow you to check the compliance of programs in the CIAO language with the requirements automatically and, thereby, check the semantics of the developed program. The proposed method narrows the specifcation formalism to the class of regular languages and the programming language to a language with a simple and predefned structure. In many practical cases, this is suffcient for effective verifcation.

верификациясобытийно-ориентированные программыразработка критических системрегулярные выражениясистема управления лифтомverifcationevent-driven programscritical system developmentregular expressionselevator control systemРабота Ирины Афанасьевой выполнена в рамках государственного задания Специальной астрофизической обсерватории РАН № 121092300060-6, утвержденного Министерством науки и высшего образования Российской Федерации.The work of Irina Afanasieva was carried out within the framework of the SAO RAS State Assignment approved by the Ministry of Science and Higher Education of the Russian Federation no. 121092300060-6.ReferencesHarel D., Pnueli D. On the development of reactive systems // Logics and Models of Concurrent Systems. Berlin, Heidelberg: Springer, 1985. P. 477–498. https://doi.org/10.1007/978-3-642-82453-1_17Harel D., Pnueli D. On the development of reactive systems. Logics and Models of Concurrent Systems. Berlin, Heidelberg, Springer, 1985, pp. 477–498. https://doi.org/10.1007/978-3-642-82453-1_17Карпов Ю.Г. Model Checking. Верификация параллельных и распределенных программных систем. СПб.: БХВ-Петербург, 2010. 560 с.Karpov Iu.G. Model Checking. Verifcation of Parallel and Distributed Software Systems. St. Petersburg, BHV-Petersburg Publ., 2010, 560 p. (in Russian)Sommerville I. Software Engineering / 10th ed. Boston: Pearson, 2020.Sommerville I. Software Engineering. 10th ed. Boston, Pearson, 2020.Hinchey M., Coyle L. Evolving critical systems: a research agenda for computer-based systems // Proc. of the 17th IEEE International Conference and Workshops on Engineering of Computer Based Systems. 2010. P. 430–435. https://doi.org/10.1109/ECBS.2010.56Hinchey M., Coyle L. Evolving critical systems: a research agenda for computer-based systems. Proc. of the 17th IEEE International Conference and Workshops on Engineering of Computer Based Systems, 2010, pp. 430–435. https://doi.org/10.1109/ECBS.2010.56Вельдер С.Э., Лукин М.А., Шалыто А.А., Яминов Б.Р. Верификация автоматных программ. СПб.: Наука, 2011. 244 с.Velder S.E., Lukin M.A., Shalyto A.A., Iaminov B.R. Automata-Based Program Verifcation. St. Petersburg, Nauka Publ., 2011, 244 p. (in Russian)Fedorchenko L., Baranov S. Equivalent transformations and regularization in context-free grammars // Cybernetics and Information Technologies. 2015. V. 14. N 4. P. 29–44. https://doi.org/10.1515/cait-2014-0003Fedorchenko L., Baranov S. Equivalent transformations and regularization in context-free grammars. Cybernetics and Information Technologies, 2015, vol. 14, no. 4, pp. 29–44. https://doi.org/10.1515/cait-2014-0003Новиков Ф.А., Афанасьева И.В. Кооперативное взаимодействие автоматных объектов // Информационно-управляющие системы. 2016. № 6. С. 50–64. https://doi.org/10.15217/issn1684-8853.2016.6.50Novikov F.A., Afanasieva I.V. Cooperative interaction of automata objects. Information and Control Systems, 2016, no. 6, pp. 50–64. (in Russian). https://doi.org/10.15217/issn1684-8853.2016.6.50Афанасьева И.В., Новиков Ф.А., Федорченко Л.Н. Методика построения событийно-управляемых программных систем с использованием языка спецификации CIAO // Труды СПИИРАН. 2020. Т. 19. № 3. С. 481–514. https://doi.org/10.15622/sp.2020.19.3.1Afanasieva I., Novikov F., Fedorchenko L. Methodology for development of event-driven software systems using ciao specifcation language. SPIIRAS Proceedings, 2020, no. 19, no. 3, pp. 481–514. (in Russian). https://doi.org/10.15622/sp.2020.19.3.1Aho A.V., Lam M.S., Sethi R., Ullman J.D. Compilers: Principles, Techniques, and Tools / 2nd ed. Boston: Pearson/Addison-Wesley, 2007. 1009 p.Aho A.V., Lam M.S., Sethi R., Ullman J.D. Compilers: Principles, Techniques, and Tools. 2nd ed. Boston, Pearson/Addison-Wesley, 2007, 1009 p.Афанасьева И.В., Новиков Ф.А. Архитектура программного обеспечения систем оптической регистрации // Информационно-управляющие системы. 2016. № 3. С. 51–63. https://doi.org/10.15217/issn1684-8853.2016.3.51Afanasieva I.V., Novikov F.A. Software architecture for optical detector systems. Information and Control Systems, 2016, no. 3, pp. 51–63. (in Russian). https://doi.org/10.15217/issn1684-8853.2016.3.51Новиков Ф.А., Иванов Д.Ю. Моделирование на UML. Теория, практика, видеокурс. СПб.: Профессиональная литература, 2010. 640 с.Novikov F.A., Ivanov D.Iu. UML Modeling. Theory, Practice, Video Course. St. Petersburg, Professional’naja literature Publ., 2010, 649 p.Knuth D.E. The Art of Computer Programming, V. 1. Fundamental Algorithms / 3rd ed. Addison-Wesley Professional, 1997. 672 p.Knuth D.E. The Art of Computer Programming, V. 1. Fundamental Algorithms. 3rd ed. Addison-Wesley Professional, 1997, 672 p.Поликарпова Н.И., Шалыто А.А. Автоматное программирование. СПб.: Питер, 2011. 176 с.Polikarpova N.I., Shalyto A.A. Automata-Based Programming. St. Petersburg, Piter Publ., 2011, 176 p. (in Russian)Fan W., Li J., Ma S., Tang N., Wu Y., Wu Y. Graph pattern matching: From intractable to polynomial time // Proceedings of the VLDB Endowment. 2010. V. 3. N 1–2. P. 264–275. https://doi.org/10.14778/1920841.1920878Fan W., Li J., Ma S., Tang N., Wu Y., Wu Y. Graph pattern matching: From intractable to polynomial time. Proceedings of the VLDB Endowment, 2010, vol. 3, no. 1–2, pp. 264–275. https://doi.org/10.14778/1920841.1920878Авдошин С.М., Набебин А.А. Дискретная математика. Формально-логические системы и языки. М.: ДМК Пресс, 2018. 390 с.Avdoshin S.M., Nabebin A.A. Discrete Mathematics. Formal Logic Systems and Languages. Moscow, DMK Press Publ., 2018, 390 p. (in Russian)Levonevskiy D., Novikov F., Fedorchenko L., Afanasieva I. Verifcation of internet protocol properties using cooperating automaton objects // Proc. of the 12th International Conference on Security of Information and Networks (SIN’19). 2019. P. 1–4. https://doi.org/10.1145/3357613.3357639Levonevskiy D., Novikov F., Fedorchenko L., Afanasieva I. Verifcation of internet protocol properties using cooperating automaton objects. Proc. of the 12th International Conference on Security of Information and Networks (SIN’19), 2019, pp. 1–4. https://doi.org/10.1145/3357613.3357639Dijkstra E.W. A Discipline of Programming / 3rd ed. Englewood Cliffs, N.J.: Prentice Hall, 1976. 217 p.Dijkstra E.W. A Discipline of Programming. 3rd ed. Englewood Cliffs, N.J., Prentice Hall, 1976, 217 p.Шалыто А.А. Валидация автоматных спецификаций // Научно-технический вестник информационных технологий, механики и оптики. 2023. Т. 23. № 2. С. 436–438. https://doi.org/10.17586/2226-1494-2023-23-2-436-438Shalyto A.A. Validation of state machine specifcations. Scientifc and Technical Journal of Information Technologies, Mechanics and Optics, 2023, vol. 23, no. 2, pp. 436–438. (in Russian). https://doi.org/10.17586/2226-1494-2023-23-2-436-438

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