Other dead states belong to livelocks where
the program cycles without making progress. In this FSM, we find the same cycle
of actions with no escape that we found in the InitialOutOfRangeMessage run:
Timeout, Reset, Message, CheckMessage (Figure 3.11).
Overview 51
0
2
Timeout()
1
Command()
3
Reset()
6
Message("999.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 3.11. Portion of controller FSM showing livelock.
52 Why We Need Model-Based Analysis
This FSM expresses all possible behaviors of the controller, so the analysis here
is complete and conclusive. This is possible because our control program has only
a few variables, each with just a few values, so it can be explored exhaustively
(completely). Our techniques can also be applied to systems that cannot be explored
exhaustively. We can configure exploration to achieve a degree of coverage that,
although incomplete, is still capable of revealing many defects (Chapter 11).
3.8 Exercises
1. Write down another run that could be executed by the controller code, which
violates the safety requirement given at the beginning of Section 3.
Pages:
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93