9") Message("99.9")
110
TimeoutMsgLate()
111
TimeoutMsgLost()
109
Command()
116
ReportLostMessage()
115
ReportLostMessage()
112
NoHandler()
Message("999.9") Message("99.9") TimeoutMsgLate() TimeoutMsgLost()
Command()
Command()
Timeout()
Command()
Message("99.9")
Message("999.9")
TimeoutMsgLost()
118
TimeoutMsgLate()
Poll()
Command()
Message("99.9")
Message("999.9")
TimeoutMsgLost()
TimeoutMsgLate()
Command()
TimeoutMsgLost()
Message("99.9")
TimeoutMsgLate() Message("999.9")
Command()
Timeout()
20
Command()
21
NoHandler() Command()
Command()
Message("999.9")TimeoutMsgLost() Message("99.9") TimeoutMsgLate()
Figure 6.9. Reactive system: true FSM showing unsafe states.
This example confirms that model-based analysis reveals one of the design errors
we originally discovered by executing the implementation.
6.3.2 Liveness
Liveness analysis checks whether something good will happen. It searches for dead
states from which goals cannot be reached. We express liveness requirements by
identifying accepting states, where goals have been reached. We define accepting
states by writing an accepting state condition, a Boolean expression that is supposed
to be true in every accepting state. A dead state is a state from which an accepting
state cannot be reached. For the tools, an accepting state condition is a Boolean
field, property, or method labeled with the [AcceptingStateCondition] attribute.
Pages:
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167