9")
7
Message("99.9")
5
TimeoutMsgLate()
4
Command()
8
TimeoutMsgLost()
9
CheckMessage()
11
Command()
12
Timeout()
23
Poll()
28
TimeoutMsgLost()
25
TimeoutMsgLate()
24
Command()
26
Message("999.9")
27
Message("99.9")
29
CheckMessage()
54
Timeout()
53
Command()
56
Reset()
58
TimeoutMsgLate()
57
Command()
60
Message("99.9")
61
TimeoutMsgLost()
59
Message("999.9")
CheckMessage()
Figure 6.13. Reactive system: interactive exploration showing path to livelock.
Systems with Finite Models 113
0
1
Command()
2
Timeout()
3
Reset()
4
Command()
7
Message("99.9")
5
TimeoutMsgLate()
6
Message("999.9")
8
TimeoutMsgLost()
19
NoHandler()
20
Command()
21
NoHandler() Command()
Figure 6.14. Reactive system: interactive exploration showing path to deadlock.
We also reproduce the LostMessageWhenIdle run, where the program reaches
a deadlocks (Figure 6.14). The deadlock is indicated by the loop of alternating
Command and NoHandler actions, from which there is no escape. The deadlock here
is a loop rather than a dead end. The supervisor can always command the controller,
so the Command action is always enabled. But the controller can do nothing; recall
that NoHandler is a dummy action that indicates no handlers are enabled.
These examples confirm that model-based analysis reveals the design errors we
originally discovered by executing the implementation.
Pages:
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174