9")
99
Command()
104
NoHandler()
Command()
106
Timeout()
Figure 3.9. Portion of controller FSM showing path to unsafe state.
out-of-range. Figure 3.8 shows the entire FSM; the filled-in ovals are the unsafe
states. (It is not necessary to search the graph visually to find out whether there are
any unsafe states; the tool writes a message to report that it finds four of them.)
Figure 3.9 shows the portion of the FSM that includes the path to an unsafe state
traversed by the OutOfRangeMessageWhenIdle run.
50 Why We Need Model-Based Analysis
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 3.10. Portion of controller FSM showing deadlock.
For liveness analysis, the tool can search for dead states from which the controller
cannot reach any accepting states where the program??™s goals have been achieved.
The most obvious dead states are deadlock states: the program stops, as in the
LostMessageWhenIdle run (Figure 3.10). The deadlock is indicated here by the loop
of alternating Command and NoHandler actions, from which there is no escape. 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.
Pages:
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92