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

Приведем результат проверки, осуществляемой разработанной си-

стемой.

[AG(AF(Error|Opened))]

Subformulas:

#sub1= Error

#sub2= Opened

#sub3= #sub1|#sub2

#sub4= AF #sub3

#sub5= / #sub4

#sub6= E(#sub0 U #sub5)

#sub7= / #sub6

#sub1 #sub2 #sub3 #sub4 #sub5 #sub6 #sub7

State 36: 0 0 0

1

0 0

1

Result of verification is positive for the initial state of the graph

(state 36)

[AG(AF(Error|Closed))]

Subformulas:

#sub1= Error

#sub2= Closed

#sub3= #sub1|#sub2

#sub4= AF #sub3

#sub5= / #sub4

#sub6= E(#sub0 U #sub5)

#sub7= / #sub6

#sub1 #sub2 #sub3 #sub4 #sub5 #sub6 #sub7

State 36: 0 1

1

0 1

0

Result of verification is negative for the initial state of the graph

(state 36)

Результат проверки, выполненной с помощью системы верифика-

ции, совпадает с полученным теоретически.

Временн´oй автомат.

Для проверки работы системы с временн ´ыми

автоматами используем пример, приведенный в работе [8].

Для временн´oго автомата, приведенного на рис. 6, проверяется

формула Ф= AG

<

=1

n. В работе [8] доказывается, что данная формула

не выполняется для этого автомата. Приведем результат проверки,

осуществляемой разработанной системой.

ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012

55