Стр. 5 - А.М. Андреев, И.А. Козлов - Подход к верификации моделей систем реального времени с помощью метода Model Checking

Рис. 4. Граф временных зон (слева); зоны Z1 и Z 2 во временн´ом пространстве
с двумя часами (справа)
Наконец, после завершения процедуры верификации строится при-
мер, подтверждающий правильность проверки системы. После этого
подтверждающая трасса (контрпример) представляется в терминах ис-
ходной программы.
Применение системы верификации. Автоматные программы.
В основе разработанной системы лежит метод верификации моделей
программ. Поэтому она наилучшим образом подходит для верифи-
кации программ, построение моделей которых просто автоматизиро-
вать, обеспечивая при этом максимальную адекватность построенной
модели оригиналу. Этим требованиям отвечают программы, создан-
ные с использованием автоматного подхода [6, 7]. Такие программы
можно верифицировать с помощью проверки моделей проще и эф-
фективнее, чем программы других классов. Поэтому при разработ-
ке системы верификации была предусмотрена возможность проверки
таких программ — при описании входной модели можно использо-
вать все компоненты, используемые при автоматном подходе: события
(инициирующие переходы между состояниями), входные воздействия
(условия переходов), выходные воздействия (действия, выполняемые
при попадании в определенное состояние или при успешном переходе
по определенному ребру), условия на состояния внешних автоматов.
Временн ´ые автоматы. Разработанная система верификации изна-
чально рассматривалась как средство проверки автоматных программ.
Однако при проектировании подобной системы конечной целью долж-
на быть возможность проверки программ общего вида. Выясним, осу-
ществима ли такая проверка в созданной системе.
Очевидно, что она не предназначена для верификации программ,
написанных с помощью традиционных языков программирования, в
исходном виде необходимо преобразование их к форме, понятной ве-
рификатору. Для программ, критичных ко времени, такой формой мо-
жет являться временн´oй автомат — это стандартный формализм для
моделирования и анализа асинхронных систем реального времени.
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012 51