ntvНаучно-технический вестник информационных технологий, механики и оптикиScientific and Technical Journal of Information Technologies, Mechanics and Optics2226-14942500-0373Университет ИТМО10.17586/2226-1494-2025-25-2-328-338ntv-453Research ArticleКОМПЬЮТЕРНЫЕ СИСТЕМЫ И ИНФОРМАЦИОННЫЕ ТЕХНОЛОГИИCOMPUTER SCIENCEПроверка соответствия поведения системы на основе автоматных объектов формальным требованиямVerification of the formal requirements for the system behavior based on automaton objectshttps://orcid.org/0000-0003-4450-0173НовиковФ. А.NovikovF. A.

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

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

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

Saint Petersburg, 195251; sc 16441904500

fedornovikov51@gmail.comhttps://orcid.org/0000-0003-4225-4124АфанасьеваИ. В.AfanasievaI. V.

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

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

Irina V. Afanasieva — PhD, Head of Laboratory.

Nizhny Arkhyz, 369167, sc 57210431774

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

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

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

Ludmila N. Fedorchenko — PhD, Senior Researcher.

Saint Petersburg, 199178, sc 36561350100

lnf@iias.spb.suhttps://orcid.org/0009-0002-3456-0471ХарисоваТ. А.KharisovaT. A.

Харисова Таисия Анваровна — инженер.

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

Taisia A. Kharisova — Engineer.

Saint Petersburg, 194021

tais.harisova@mail.ruСанкт-Петербургский политехнический университет Петра ВеликогоРоссияPeter the Great St. Petersburg Polytechnic UniversityRussian FederationСпециальная астрофизическая обсерватория Российской академии наукРоссияSpecial Astrophysical Observatory of the Russian Academy of Sciences (SAO RAS)Russian FederationСанкт-Петербургский Федеральный исследовательский центр Российской академии наукРоссияSt. Petersburg Federal Research Center of the Russian Academy of SciencesRussian FederationФизико-технический институт им. А.Ф. Иоффе Российской академии наукРоссияIoffe InstituteRussian Federation202524042025252328338Copyright © Новиков Ф.А., Афанасьева И.В., Федорченко Л.Н., Харисова Т.А., 20252025Новиков Ф.А., Афанасьева И.В., Федорченко Л.Н., Харисова Т.А.Novikov F.A., Afanasieva I.V., Fedorchenko L.N., Kharisova T.A.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://ntv.elpub.ru/jour/article/view/453Введение

Введение. В работе исследованы проблемы автоматической проверки соответствия поведения реагирующей системы формализованным требованиям, а именно, автоматической верификации. Реагирующая система описывается в форме взаимосвязанных автоматных объектов. Формализованные требования записываются в виде обусловленных регулярных выражений. Показано, что в этом случае возможна математически достоверная верификация системы.

Метод

Метод. Предложенное решение основано на применении языка спецификации взаимодействия автоматных объектов Cooperative Interaction of Automaton Objects (CIAO). В данной работе рассматривается третья версия языка, CIAO v.3, в котором определены средства описания автоматных классов, средства инстанциации автоматных объектов и связывания этих объектов в систему с помощью схемы связей. Верифицируемые требования заданы с помощью так называемых обусловленных регулярных выражений, построенных над множеством элементарных действий и условий, определенных в системе. Разработан программный инструмент, который, используя схему связей, строит семантический граф — ориентированный граф, в котором все пути из начальных узлов представляют протоколы выполнения автоматной программы, задавая тем самым семантику реагирующей системы. Выполнена проверка соответствия автоматной программы требованию, определяемому обусловленным регулярным выражением. В случае обнаружения несоответствия инструмент показывает место, где именно семантический граф не соответствует требованию.

Основные результаты

Основные результаты. Разработаны алгоритмы, позволяющие проводить автоматическую верификацию реагирующих систем относительно формализованных требований определенного класса. Рассмотрен пример программы, демонстрирующий управление работой лифта на языке CIAO v.3 и проведена верификация построенной реагирующей системы на соответствие формально заданным требованиям. Обсуждение. Продемонстрирована программная реализации инструмента автоматической верификации программы на языке CIAO v.3.

The paper studies the problems of automatic verification of the behavior of a reactive system in accordance with formalized requirements, i.e., automatic verification. The reactive system is described by interconnected automaton objects. Formalized requirements are written as conditioned regular expressions. In this case mathematically reliable verification of the system is possible. The proposed solution is based on the use of the CIAO (Cooperative Interaction of Automaton Objects) language to specify the interaction of automaton objects. This paper considers the third version of the language, CIAO v.3, which defines the means of describing automaton classes, the means of instantiating automaton objects, and linking these objects to the system using a link diagram. The requirements to be verified are specified using the so-called conditioned regular expressions constructed over a set of elementary actions and conditions defined in the system. A software tool has been developed that, using a link diagram, builds a semantic graph, i.e., a directed graph, where all paths from the initial nodes represent the execution protocols of the automata-based program, thereby specifying the semantics of the reactive system. Then, it is checked whether the automata-based program complies with the requirement defined by the conditioned regular expression. If a discrepancy is detected, the tool shows the place where the semantic graph exactly does not comply with the requirement. Algorithms have been developed that allow automatic verification of reactive systems with respect to the formalized requirements of a certain class. An example of a program is given that demonstrates elevator control in the CIAO v.3 language, and the constructed reactive system is verified for compliance with formally specified requirements. The purpose of the article is to demonstrate software implementation of the tool for automatic verification of a program in the CIAO v.3 language.

автоматическая верификацияобусловленные регулярные выражениямодель поведенияавтоматное программированиеграф переходов состоянийунифицированный язык моделирования UMLдиаграмма конечного автоматапараллельное поведениеархитектура программного обеспеченияреагирующая системаautomatic verificationconditioned regular expressionsbehavior modelautomata-based programmingstate transition graphUMLstate machine diagramconcurrent behaviorsoftware architecturereactive systemReferencesКулямин В.В. Методы верификации программного обеспечения. М.: ИСП РАН, 2008. 111 с.Kulyamin V.V. Software Verification Methods. Moscow, ISP RAS, 2008, 111 p. (in Russian)Шалыто А.А. Валидация автоматных спецификаций // Научнотехнический вестник информационных технологий, механики и оптики. 2023. Т. 23. № 2. С. 436–438. https://doi.org/10.17586/2226-1494-2023-23-2-436-438Shalyto A.A. Validation of state machine specifications. Scientific 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Лавров С.С. Программирование. Математические основы, средства, теория. СПб.: БХВ-Петербург, 2001. 320 с.Lavrov S.S. Programming. Mathematical Foundations, Tools, Theory. St. Petersburg, BHV Petersburg Publ., 2001, 320 p. (in Russian)Dijkstra E.W. A Discipline of Programming. Prentice Hall, 1976. 217 p.Dijkstra E.W. A Discipline of Programming. Prentice Hall, 1976, 217 p.Карпов Ю.Г. Model Checking. Верификация параллельных и распределенных систем. СПб.: БХВ-Петербург, 2010. 560 с.Karpov Iu.G. Model Checking. Verification of Parallel and Distributed Software Systems. St. Petersburg, BHV-Petersburg, 2010, 560 p. (in Russian)Виноградов Р.А., Кузьмин Е.В., Соколов В.А. Верификация автоматных программ средствами CPN/Tools // Моделирование и анализ информационных систем. 2006. Т. 13. № 2. С. 4–15.Vinogradov R.A., Kuz’min E.V., Sokolov V.A. Verification of automata programs using CPN/Tools. Modelirovanie i analiz informacionnyh sistem, 2006, vol. 13, no. 2, pp. 4–15. (in Russian)Шалыто А.А. Парадигма автоматного программирования // Научно-технический вестник Санкт-Петербургского государственного университета информационных технологий, механики и оптики. 2008. № 53. С. 3–23.Shalyto A. Automata-based programming paradigm. Scientific and Technical Journal of Information Technologies, Mechanics and Optics, 2008, vol. 53, pp. 3–23. (in Russian)Поликарпова Н.И., Шалыто А.А. Автоматное программирование. СПб.: Питер, 2010. 176 с.Polikarpova N.I., Shalyto A.A. Automata-Based Programming. St. Petersburg, Piter Publ., 2011, 176 p. (in Russian)Новиков Ф.А., Тихонова У.Н. Автоматный метод определения проблемно-ориентированных языков. Ч. 1 // Информационно-управляющие системы. 2009. № 6 (43). С. 34–40.Novikov F.A., Tikhonova U.N. An Automata Based Method for Domain Specific Languages Definition. Part 1. Information and Control Systems, 2009, no. 6 (43), pp. 34–40. (in Russian)Новиков Ф.А., Тихонова У.Н. Автоматный метод определения проблемно-ориентированных языков. Ч. 2 // Информационно-управляющие системы. 2010. № 2 (45). С. 31–37.Novikov F.A., Tikhonova U.N. An Automata Based Method for Domain Specific Languages Definition. Part 2. Information and Control Systems, 2010, no. 2 (45), pp. 31–37. (in Russian)Новиков Ф.А., Тихонова У.Н. Автоматный метод определения проблемно-ориентированных языков. Ч. 3 // Информационно-управляющие системы. 2010. № 3(46). С. 29–37.Novikov F.A., Tikhonova U.N. An Automata Based Method for Domain Specific Languages Definition. Part 3. Information and Control Systems, 2010, no. 3 (46), pp. 29–37. (in Russian)Novikov F., Fedorchenko L., Vorobiev V., Fatkieva R., Levonevskiy D. Attribute-based approach of defining the secure behavior of automata objects // Proc. of the 10th International Conference on Security of Information and Networks (SIN’17). 2017. P. 67–72. https://doi.org/10.1145/3136825.3136887Novikov F., Fedorchenko L., Vorobiev V., Fatkieva R., Levonevskiy D. Attribute-based approach of defining the secure behavior of automata objects. Proc. of the 10th International Conference on Security of Information and Networks (SIN’17), 2017, pp. 67–72. https://doi.org/10.1145/3136825.3136887Новиков Ф.А., Афанасьева И.В. Кооперативное взаимодействие автоматных объектов // Информационно-управляющие системы. 2016. № 6 (85). С. 50–64. https://doi.org/10.15217/issn1684-8853.2016.6.50Novikov F.A., Afanasyeva I.V. Cooperative interaction of automata objects. Information and control systems, 2016, no. 6 (85), pp. 50–64. (in Russian). https://doi.org/10.15217/issn1684-8853.2016.6.50Afanasieva I.V. Data acquisition and control system for highperformance large-area CCD Systems // Astrophysical Bulletin. 2015. V. 70. N 2. P. 232–237. https://doi.org/10.1134/S1990341315020108Afanasieva I.V. Data acquisition and control system for highperformance large-area CCD Systems. Astrophysical Bulletin, 2015, vol. 70, no. 2, pp. 232–237. https://doi.org/10.1134/s1990341315020108Levonevskiy D., Novikov F., Fedorchenko L., Afanasieva I. Verification 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. Verification 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.3357639Афанасьева И.В., Новиков Ф.А., Федорченко Л.Н. Методика построения событийно-управляемых программных систем с использованием языка спецификации CIAO // Труды СПИИРАН. 2020. Т. 19. № 3. С. 481–514. https://doi.org/10.15622/sp.2020.19.3.1Afanasyeva I.V., Novikov F.A., Fedorchenko L.N. Methodology for constructing event-driven software systems using the CIAO specification language. SPIIRAS Proceedings, 2020, vol. 19, no. 3, pp. 481–514. (in Russian). https://doi.org/10.15622/sp.2020.19.3.1Afanasieva I.V., Novikov F.A., Fedorchenko L.N. Verification of event-driven software systems using the specification language of cooperating automata objects //scientific and Technical Journal of Information Technologies, Mechanics and Optics. 2023. V. 23. N 4. P. 750–756. https://doi.org/10.17586/2226-1494-2023-23-4-750-756Afanasieva I.V., Novikov F.A., Fedorchenko L.N. Verification of event-driven software systems using the specification language of cooperating automata objects. Scientific and Technical Journal of Information Technologies, Mechanics and Optics, 2023, vol. 23, no. 4, pp. 750–756. https://doi.org/10.17586/2226-1494-2023-23-4-750-756Новиков Ф.А., Афанасьева И.В., Федорченко Л.Н., Харисова Т.А. Применение условных регулярных выражений в задачах верификации управляющих автоматных программ. Сборник научных трудов XIV Всероссийского совещания по проблемам управления. М.: ИПУ РАН, 2024. С. 2651–2655.Novikov F.A., Afanasyeva I.V., Fedorchenko L.N., Kharisova T.A. Application of conditional regular expressions in problems of verification of control automata programs. 14th All-Russian conference on control problems. Collection of Scientific Papers. Moscow, IPU RAS, 2024, pp. 2651–2655. (in Russian)Novikov F.A., Afanasieva I.V., Fedorchenko L.N., Kharisova T.A. Specification language for automatаbased objects cooperation //scientific and Technical Journal of Information Technologies, Mechanics and Optics. 2024. V. 24. N 6. P. 1035–1043. https://doi.org/10.17586/2226-1494-2024-24-6-1035-1043Novikov F.A., Afanasieva I.V., Fedorchenko L.N., Kharisova T.A. Specification language for automatаbased objects cooperation. Scientific and Technical Journal of Information Technologies, Mechanics and Optics, 2024, vol. 24, no. 6, pp. 1035–1043. https://doi.org/10.17586/2226-1494-2024-24-6-1035-1043Новиков Ф.А., Афанасьева И.В., Федорченко Л.Н., Харисова Т.А. Применение условных регулярных выражений в задачах верификации управляющих автоматных программ. Сборник материалов Всероссийской научной конференции “Неделя науки ФизМех”. СПб.: ПОЛИТЕХ-ПРЕСС, 2024. С. 167–170.Novikov F.A., Afanasyeva I.V., Fedorchenko L.N., Kharisova T.A. Application of Conditional Regular Expressions in Verification Problems of Control Automata Programs. Proc. of Materials of the All-Russian Scientific Conference “PhysMech Science Week”, St. Petersburg, POLYTECH-PRESS, 2024, pp. 167–170. (in Russian)Новиков Ф.А., Иванов Д.Ю. Моделирование на UML. Теория, практика, видеокурс. СПб.: Профессиональная литература, 2010. 640 с.Novikov F.A., Ivanov D.Iu. UML Modeling. Theory, Practice, Video Course. St. Petersburg, Professional’naja literature Publ., 2010, 640 p. (in Russian)Шалыто А.А. Switch-технология. Алгоритмизация и программирование задач логического управления. СПб.: Наука, 1998. 617 с.Shalyto A.A. Switch-Technology. Algorithmization and Programming of the Logical Control Problems. St. Petersburg, Nauka Publ., 1998, 617 p. (in Russian)Вельдер С.Э., Шалыто А.А. Методы верификации моделей автоматных программ // Научно-технический вестник Санкт-Петербургского государственного университета информационных технологий, механики и оптики. 2008. № 53. С. 123–137.Velder S.E., Shalyto A.A. Methods of verification of models of automata-based programs. Scientific and Technical Journal of Information Technologies, Mechanics and Optics, 2008, vol. 53, pp. 123–137. (in Russian)Вельдер С.Э., Лукин М.А., Шалыто А.А., Яминов Б.Р. Верификация автоматных программ. СПб.: Наука, 2011. 244 с.Velder S.E., Lukin M.A., Shalyto A.A., Iaminov B.R. Verification of Automata-Based Programs. St. Petersburg, Nauka Publ., 2011, 244 p. (in Russian)Кузьмин Е.В., Соколов В.А. Моделирование, спецификация и верификация «автоматных» программ // Программирование. 2008. Т. 34. № 1. С. 38–60.Kuzmin E.V., Sokolov V.A. Modeling, specification, and verification of automaton programs. Programming and Computer Software, 2008, vol. 34, no. 1, pp. 27–43. https://doi.org/10.1134/s0361768808010040Гамма Э., Хелм Р., Джонсон Р., Влиссидес Д. Паттерны объектно-ориентированного проектирования. СПб.: Питер, 2020. 448 с.Gamma E., Helm R., Johnson R., Vlissides J. Design Patterns: Elements of Reusable Object-Oriented Software. Pearson Education, 1994, 416 p.Герасимов А.Ю. Направленное динамическое символьное исполнение программ для подтверждения ошибок в программах // Программирование. 2018. № 5. C. 31–42. https://doi.org/10.31857/s013234740001213-9Gerasimov A.Y. Directed dynamic symbolic execution for static analysis warnings confirmation. Programming and Computer Software, 2018, vol. 44, no. 5, pp. 316–323. https://doi.org/10.1134/s036176881805002XFriedl J.E.F. Mastering Regular Expressions: Understand Your Data and Be More. O’Reilly Media, Inc., 2006. 544 p.Friedl J.E.F. Mastering Regular Expressions: Understand Your Data and Be More. O’Reilly Media, Inc., 2006, 544 p.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

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