Проверка соответствия поведения системы на основе автоматных объектов формальным требованиям

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

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

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

1. Кулямин В.В. Методы верификации программного обеспечения. М.: ИСП РАН, 2008. 111 с.

2. Шалыто А.А. Валидация автоматных спецификаций // Научнотехнический вестник информационных технологий, механики и оптики. 2023. Т. 23. № 2. С. 436–438. https://doi.org/10.17586/2226-1494-2023-23-2-436-438

3. Лавров С.С. Программирование. Математические основы, средства, теория. СПб.: БХВ-Петербург, 2001. 320 с.

4. Dijkstra E.W. A Discipline of Programming. Prentice Hall, 1976. 217 p.

5. Карпов Ю.Г. Model Checking. Верификация параллельных и распределенных систем. СПб.: БХВ-Петербург, 2010. 560 с.

6. Виноградов Р.А., Кузьмин Е.В., Соколов В.А. Верификация автоматных программ средствами CPN/Tools // Моделирование и анализ информационных систем. 2006. Т. 13. № 2. С. 4–15.

7. Шалыто А.А. Парадигма автоматного программирования // Научно-технический вестник Санкт-Петербургского государственного университета информационных технологий, механики и оптики. 2008. № 53. С. 3–23.

8. Поликарпова Н.И., Шалыто А.А. Автоматное программирование. СПб.: Питер, 2010. 176 с.

9. Новиков Ф.А., Тихонова У.Н. Автоматный метод определения проблемно-ориентированных языков. Ч. 1 // Информационно-управляющие системы. 2009. № 6 (43). С. 34–40.

10. Новиков Ф.А., Тихонова У.Н. Автоматный метод определения проблемно-ориентированных языков. Ч. 2 // Информационно-управляющие системы. 2010. № 2 (45). С. 31–37.

11. Новиков Ф.А., Тихонова У.Н. Автоматный метод определения проблемно-ориентированных языков. Ч. 3 // Информационно-управляющие системы. 2010. № 3(46). С. 29–37.

12. 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.3136887

13. Новиков Ф.А., Афанасьева И.В. Кооперативное взаимодействие автоматных объектов // Информационно-управляющие системы. 2016. № 6 (85). С. 50–64. https://doi.org/10.15217/issn1684-8853.2016.6.50

14. Afanasieva 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/S1990341315020108

15. Levonevskiy 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.3357639

16. Афанасьева И.В., Новиков Ф.А., Федорченко Л.Н. Методика построения событийно-управляемых программных систем с использованием языка спецификации CIAO // Труды СПИИРАН. 2020. Т. 19. № 3. С. 481–514. https://doi.org/10.15622/sp.2020.19.3.1

17. Afanasieva 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-756

18. Новиков Ф.А., Афанасьева И.В., Федорченко Л.Н., Харисова Т.А. Применение условных регулярных выражений в задачах верификации управляющих автоматных программ. Сборник научных трудов XIV Всероссийского совещания по проблемам управления. М.: ИПУ РАН, 2024. С. 2651–2655.

19. 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-1043

20. Новиков Ф.А., Афанасьева И.В., Федорченко Л.Н., Харисова Т.А. Применение условных регулярных выражений в задачах верификации управляющих автоматных программ. Сборник материалов Всероссийской научной конференции “Неделя науки ФизМех”. СПб.: ПОЛИТЕХ-ПРЕСС, 2024. С. 167–170.

21. Новиков Ф.А., Иванов Д.Ю. Моделирование на UML. Теория, практика, видеокурс. СПб.: Профессиональная литература, 2010. 640 с.

22. Шалыто А.А. Switch-технология. Алгоритмизация и программирование задач логического управления. СПб.: Наука, 1998. 617 с.

23. Вельдер С.Э., Шалыто А.А. Методы верификации моделей автоматных программ // Научно-технический вестник Санкт-Петербургского государственного университета информационных технологий, механики и оптики. 2008. № 53. С. 123–137.

24. Вельдер С.Э., Лукин М.А., Шалыто А.А., Яминов Б.Р. Верификация автоматных программ. СПб.: Наука, 2011. 244 с.

25. Кузьмин Е.В., Соколов В.А. Моделирование, спецификация и верификация «автоматных» программ // Программирование. 2008. Т. 34. № 1. С. 38–60.

26. Гамма Э., Хелм Р., Джонсон Р., Влиссидес Д. Паттерны объектно-ориентированного проектирования. СПб.: Питер, 2020. 448 с.

27. Герасимов А.Ю. Направленное динамическое символьное исполнение программ для подтверждения ошибок в программах // Программирование. 2018. № 5. C. 31–42. https://doi.org/10.31857/s013234740001213-9

28. Friedl J.E.F. Mastering Regular Expressions: Understand Your Data and Be More. O’Reilly Media, Inc., 2006. 544 p.

29. 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-0003