Верификация событийно-управляемых программных систем с использованием языка спецификации взаимодействующих автоматных объектов

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

1. Harel 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_17

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

3. Sommerville I. Software Engineering / 10th ed. Boston: Pearson, 2020.

4. 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.56

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

6. 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

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

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

9. 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.

10. Афанасьева И.В., Новиков Ф.А. Архитектура программного обеспечения систем оптической регистрации // Информационно-управляющие системы. 2016. № 3. С. 51–63. https://doi.org/10.15217/issn1684-8853.2016.3.51

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

12. Knuth D.E. The Art of Computer Programming, V. 1. Fundamental Algorithms / 3rd ed. Addison-Wesley Professional, 1997. 672 p.

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

14. 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.1920878

15. Авдошин С.М., Набебин А.А. Дискретная математика. Формально-логические системы и языки. М.: ДМК Пресс, 2018. 390 с.

16. 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.3357639

17. Dijkstra E.W. A Discipline of Programming / 3rd ed. Englewood Cliffs, N.J.: Prentice Hall, 1976. 217 p.

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