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

Рис. 2. Дерево подформул TCTL-
формулы
исходной системы. Также на этом
этапе решается еще одна задача: в
случае использования в програм-
ме нескольких параллельно дей-
ствующих автоматов, необходимо
построить их параллельную ком-
позицию.
Затем осуществляется даль-
нейшее преобразование модели:
по временн´oму автомату строит-
ся граф временных зон. Каждой
вершине графа соответствует од-
на из локаций автомата, постро-
енного на предыдущем этапе, а
также временн´aя зона — область
временн´oго пространства, все эле-
менты которой эквивалентны от-
носительно условий некоторой конкретной задачи. Зоны выбираются
так, чтобы интерпретации часов удовлетворяли заданным временным
ограничениям (рис. 4).
В результате преобразования получим граф временн ´ых зон, про-
верка которого на соответствие TCTL-формуле может быть проведена
посредством того же алгоритма, который используется для модели
Крипке и нетаймированной CTL-логики. Его базовая идея состоит
в пометке каждого состояния подформулами, которые верны в этом
состоянии. Эта процедура выполняется итеративно и завершается по-
меткой состояний, в которых выполняется сама формула ϕ. Считается,
что формула выполняется для данной модели, если в число помечен-
ных состояний входит начальное.
Рис. 3. Временной автомат
50 ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012