Рис. 1. Схема процесса верификации систем реального времени
Построение верифицируемой модели осуществляется в два этапа:
первый шаг аналогичен построению структуры Крипке для верифика-
торов общего назначения; однако, учитывая специфику систем реаль-
ного времени, необходимо использовать более сложную модель. В ка-
честве спецификационного формализма для систем реального времени
вводится понятие временн´oго автомата — расширения конечного ав-
томата, в котором для измерения времени используются часы (рис. 3).
Состояние временн´oго автомата представляет собой пару
h
s, v
i
, где
s
— локация (соответствующая позиции в невременн´oм конечном авто-
мате), а
v
— совокупность значений часов. Такой выбор модели позво-
ляет перенести на нее инварианты состояний и ограничения переходов
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012
49
1,2 4,5,6,7,8,9,10,11,12,13,...14