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

• Конечный автомат — преобразователь должен содержать множе-
ство состояний, входной и выходной алфавиты, а также отношение
переходов и выходов. В качестве входного алфавита используются
события. Роль выходных символов играют выходные воздействия в
состояниях (для автомата Мура) или на переходах (автомат Мили).
Входные воздействия не используются.
• Конечный автомат — распознаватель, в отличие от преобразовате-
ля, включает в себя множество допускающих состояний, но не имеет
выходного алфавита. Для верификации автоматов этого класса совсем
не используются выходные воздействия.
На основе рассмотренных особенностей использования верифика-
тора для разных классов систем можно классифицировать системы
следующим образом
Классификация систем
Признак классификации X E Z Zs Часы || Y
Класс автомата:
Мура gray red green
Мили gray gray green red gray gray gray
смешанный gray gray gray gray gray
без выходного преобразователя gray gray red red gray gray gray
Критичность ко времени:
система реального времени gray gray gray gray green gray gray
система, некритичная ко времени gray gray gray gray red gray gray
Метод взаимодействия:
обмен сообщениями gray gray gray gray gray green red
взаимодействие по номерам состояний gray gray gray gray gray red green
смешанное gray gray gray gray gray green green
Использование событий:
да gray green gray gray gray gray gray
нет gray red gray gray gray gray gray
Использование входных воздействий:
да green gray gray gray gray gray gray
нет red gray gray gray gray gray gray
П р и м е ч а н и е. X — входные воздействия; E — события; Z — выходные воздействия
на переходах; Zs — выходные воздействия в состояниях; || — параллелизм; Y —
условие на номер состояния другого автомата.
Зеленый цвет (green) ячейки означает, что соответствующий ком-
понент автоматной программы используется в данной системе, крас-
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012 53