Меню
Публикации
2025
2024
2023
2022
2021
2020
2019
2018
2017
2016
2015
2014
2013
2012
2011
2010
2009
2008
2007
2006
2005
2004
2003
2002
2001
Главный редактор

НИКИФОРОВ
Владимир Олегович
д.т.н., профессор
Партнеры
doi: 10.17586/2226-1494-2025-25-2-328-338
УДК 004.415.52, 004.434
Проверка соответствия поведения системы на основе автоматных объектов формальным требованиям
Читать статью полностью

Язык статьи - английский
Ссылка для цитирования:
Аннотация
Ссылка для цитирования:
Новиков Ф.А., Афанасьева И.В., Федорченко Л.Н., Харисова Т.А. Проверка соответствия поведения системы на основе автоматных объектов формальным требованиям // Научно-технический вестник информационных технологий, механики и оптики. 2025. Т. 25, № 2. С. 328–338 (на англ. яз.). doi: 10.17586/2226-1494-2025-25-2-328-338
Аннотация
Введение. В работе исследованы проблемы автоматической проверки соответствия поведения реагирующей системы формализованным требованиям, а именно, автоматической верификации. Реагирующая система описывается в форме взаимосвязанных автоматных объектов. Формализованные требования записываются в виде обусловленных регулярных выражений. Показано, что в этом случае возможна математически достоверная верификация системы. Метод. Предложенное решение основано на применении языка спецификации взаимодействия автоматных объектов Cooperative Interaction of Automaton Objects (CIAO). В данной работе рассматривается третья версия языка, CIAO v.3, в котором определены средства описания автоматных классов, средства инстанциации автоматных объектов и связывания этих объектов в систему с помощью схемы связей. Верифицируемые требования заданы с помощью так называемых обусловленных регулярных выражений, построенных над множеством элементарных действий и условий, определенных в системе. Разработан программный инструмент, который, используя схему связей, строит семантический граф — ориентированный граф, в котором все пути из начальных узлов представляют протоколы выполнения автоматной программы, задавая тем самым семантику реагирующей системы. Выполнена проверка соответствия автоматной программы требованию, определяемому обусловленным регулярным выражением. В случае обнаружения несоответствия инструмент показывает место, где именно семантический граф не соответствует требованию. Основные результаты. Разработаны алгоритмы, позволяющие проводить автоматическую верификацию реагирующих систем относительно формализованных требований определенного класса. Рассмотрен пример программы, демонстрирующий управление работой лифта на языке CIAO v.3 и проведена верификация построенной реагирующей системы на соответствие формально заданным требованиям. Обсуждение. Продемонстрирована программная реализации инструмента автоматической верификации программы на языке CIAO v.3.
Ключевые слова: автоматическая верификация, обусловленные регулярные выражения, модель поведения, автоматное
программирование, граф переходов состояний, унифицированный язык моделирования UML, диаграмма
конечного автомата, параллельное поведение, архитектура программного обеспечения, реагирующая система
Список литературы
Список литературы
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 high-performance 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. Новиков Ф.А., Афанасьева И.В., Федорченко Л.Н., Харисова Т.А. Применение условных регулярных выражений в задачах верификации управляющих автоматных программ. Cборник материалов Всероссийской научной конференции “Неделя науки ФизМех”. СПб.: ПОЛИТЕХ-ПРЕСС, 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