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

должен позволять проверять соответствие системы этим ограничени-
ям. Для верификации программ реального времени необходим особый
подход, включающий в себя подходящие математические модели и ал-
горитмы их построения и проверки. В качестве таких моделей может
выступать взвешенный граф, вершинам которого сопоставляется вре-
мя выполнения отдельных действий, или временной автомат.
В настоящей статье рассматривается подход к верификации систем
реального времени, основанный на пошаговом преобразовании исход-
ной модели программы к виду временн´oго автомата и последующей
проверке полученной структуры методом Model Checking.
Описание алгоритма верификации систем реального времени.
Верификация моделей программ включает в себя несколько основных
этапов: преобразование модели в структуру Крипке и построение тре-
бований к модели; собственно процесс верификации (отработку алго-
ритмов на полученных моделях); построение подтверждающих трасс
(контрпримеров) в модели Крипке, а также представление контрпри-
меров, записанных в терминах модели Крипке, в виде путей в исход-
ной модели. Общая схема процесса верификации приведена на рис. 1.
Для описания требований к системам, состояние которых изме-
няется во времени, используются темпоральные логики. Эти логи-
ки представляют собой классическую логику высказываний, расши-
ренную некоторыми темпоральными операторами, которые позволяют
описать отношения между моментами времени, в которые наступили
те или иные события. Обычно неважно, в какие именно моменты вре-
мени в системе происходят те или иные события, имеет значение лишь
порядок их наступления. Но отсутствующее количественное предста-
вление о времени существенно для спецификации систем, критичных
ко времени, а потому для этой цели нельзя использовать основные
темпоральные логики — LTL и CTL.
Одним из наиболее важных аспектов является выбор семанти-
ки временн´oй области. Поскольку в природе время имеет непрерыв-
ную структуру, наиболее естественным выбором является непрерыв-
ная временн´aя область, такая как вещественные числа. Одной из тем-
поральных логик, которые позволяют осуществлять проверку моделей
в терминах непрерывной временной области ( R+ — неотрицательные
вещественные числа), является ветвящаяся темпоральная логика ре-
ального времени Timed CTL [5]. Базовая идея TCTL состоит в ис-
пользовании временных ограничений в качестве параметров обычных
темпоральных операторов CTL.
Для проверки соответствия модели спецификации, выраженной в
виде TCTL-формулы, необходимо построить дерево ее подформул,
операторами каждой из которых являются подформулы более низкого
уровня (рис. 2).
48 ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012