ный (red) — что не используется, серый (gray) означает, что нали-
чие/отсутствие этого компонента для рассматриваемого признака не
принципиально.
На основе полученной классификации можно сделать вывод, что
разработанная система отличается высокой универсальностью, выра-
жающейся в способности верифицировать не только временные ав-
томаты, но и множество других моделей, применяемых в различных
классах программных систем.
Пример верификации систем различных классов.
Автомат-
ная программа
. Верификация автоматной программы общего вида бу-
дет демонстрироваться на примере автомата, управляющего дверьми
лифта (рис. 5).
Для этого автомата проверяются следующие утверждения.
При отсутствии ошибки состояние Opened посещается бесконеч-
ное число раз. Результат верификации данного утверждения — “Вы-
полняется”.
Ф
1
= AG(AF(Error
∨
Opened)).
При отсутствии ошибки состояние Closed посещается бесконечное
число раз. Результат верификации — “Нарушается”.
Ф
2
= AG(AF(Error
∨
Closed)).
Рис. 5. Схема связей (
а
) и граф переходов (
б
) автомата AElevator
54
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012
1,2,3,4,5,6,7 9,10,11,12,13,14