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

Новиков Ф.А., Афанасьева И.В., Федорченко Л.Н., Харисова Т.А. Проверка соответствия поведения системы на основе автоматных объектов формальным требованиям // Научно-технический вестник информационных технологий, механики и оптики. 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.

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