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

Рис. 6. Модель временн´ого автомата
AG(<=1)(n)]
Subformulas:
#sub1= n
#sub2= / #sub1
#sub3= #sub0 | #sub2
#sub4= #z<=1
#sub5= #sub2 & #sub4
#sub6= E(#sub3 U #sub5)
#sub7= / #sub6
#sub1 #sub2 #sub3 #sub4 #sub5 #sub6 #sub7
State 1: 0 1 1 0 0 0 1
State 2: 0 1 1 1 1 1 0
State 3: 1 0 1 0 0 0 1
State 4: 1 0 1 1 0 0 1
State 5: 1 0 1 0 0 0 1
State 6: 0 1 1 0 0 0 1
State 7: 0 1 1 0 0 0 1
State 8: 0 1 1 0 0 0 1
State 9: 0 1 1 1 1 1 0
State 10: 0 1 1 1 1 1 0
Result of verification is negative for the initial state of the graph
(state 10)
Результат проверки, выполненной с помощью системы верифика-
ции, совпадает с полученным теоретически.
Невременной конечный автомат-преобразователь. В качестве
автомата-преобразователя возьмем модель поведения отца из извест-
ного примера:
Опишем поведение отца, сын которого учится в школе и приносит
двойки и пятерки. Отец не хочет хвататься за ремень каждый раз, как
только сын получит двойку, и выбирает более тонкую тактику вос-
питания. Граф поведения представлен на рис. 7. Двумя возможными
событиями являются принесенная сыном “2” или “5”.
Проверим для этого автомата следующее утверждение: “Даже
если сейчас отец наказывает сына, возможно, что в будущем он будет
56 ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012