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

Афанасьева Ирина Викторовна, Новиков Федор Александрович, Федорченко Людмила Николаевна

doi:10.17586/2226-1494-2023-23-4-750-756

2023 , ТОМ 23, НОМЕР 4 ( июль-август )

ISSN 2226-1494 (print), ISSN 2500-0373 (online)

Меню

Публикации

Главный редактор

НИКИФОРОВ
Владимир Олегович
д.т.н., профессор

Партнеры

doi: 10.17586/2226-1494-2023-23-4-750-756

УДК 004.415.52, 004.434

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

Афанасьева И.В., Новиков Ф.А., Федорченко Л.Н.

Читать статью полностью

Язык статьи - английский

Ссылка для цитирования:

Афанасьева И.В., Новиков Ф.А., Федорченко Л.Н. Верификация событийно- управляемых программных систем с использованием языка спецификации взаимодействующих автоматных объектов // Научно-технический вестник информационных технологий, механики и оптики. 2023. Т. 23, № 4. С. 750–756 (на англ. яз.). doi: 10.17586/2226-1494-2023-23-4-750-756

Аннотация

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

Ключевые слова: верификация, событийно-ориентированные программы, разработка критических систем, регулярные выражения, система управления лифтом

Благодарности. Работа Ирины Афанасьевой выполнена в рамках государственного задания Специальной астрофизической обсерватории РАН № 121092300060-6, утвержденного Министерством науки и высшего образования Российской Федерации.

Список литературы

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
Карпов Ю.Г. Model Checking. Верификация параллельных и распределенных программных систем. СПб.: БХВ-Петербург, 2010. 560 с.
Sommerville I. Software Engineering / 10^th ed.Boston: Pearson, 2020.
Hinchey M., Coyle L. Evolving critical systems: a research agenda for computer-based systems // Proc. of the 17^th IEEE International Conference and Workshops on Engineering of Computer Based Systems. 2010. P. 430–435. https://doi.org/10.1109/ECBS.2010.56
Вельдер С.Э., Лукин М.А., Шалыто А.А., Яминов Б.Р. Верификация автоматных программ. СПб.: Наука, 2011. 244 с.
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
Новиков Ф.А., Афанасьева И.В. Кооперативное взаимодействие автоматных объектов // Информационно-управляющие системы. 2016. № 6. С. 50–64. 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.1
Aho A.V., Lam M.S., Sethi R., Ullman J.D.Compilers: Principles, Techniques, and Tools / 2^nd ed.Boston: Pearson/Addison-Wesley, 2007. 1009 p.
Афанасьева И.В., Новиков Ф.А. Архитектура программного обеспечения систем оптической регистрации // Информационно-управляющие системы. 2016. № 3. С. 51–63. https://doi.org/10.15217/issn1684-8853.2016.3.51
Новиков Ф.А., Иванов Д.Ю. Моделирование на UML. Теория, практика, видеокурс. СПб.: Профессиональная литература, 2010. 640 с.
Knuth D.E. The Art of Computer Programming, V. 1. Fundamental Algorithms / 3^rd ed.Addison-Wesley Professional, 1997. 672 p.
Поликарпова Н.И., Шалыто А.А. Автоматное программирование. СПб.: Питер, 2011. 176 с.
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
Авдошин С.М., Набебин А.А. Дискретная математика. Формально-логические системы и языки. М.: ДМК Пресс, 2018. 390 с.
Levonevskiy D., Novikov F., Fedorchenko L., Afanasieva I. Verification of internet protocol properties using cooperating automaton objects // Proc. of the 12^th International Conference on Security of Information and Networks (SIN'19). 2019. P. 1–4. https://doi.org/10.1145/3357613.3357639
Dijkstra E.W. A Discipline of Programming / 3^rd 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-438

This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License