Systems with Finite Models 109
0
2
Timeout()
1
Command()
105
107
Calibrate()
3
Reset()
6
Message("999.9")
7
Message("99.9")
4
Command()
5
TimeoutMsgLate()
8
TimeoutMsgLost()
10
CheckMessage()
72
Timeout()
71
Command()
73
Poll()
75
TimeoutMsgLate()
76
Message("999.9")
74
Command()
78
TimeoutMsgLost()
77
Message("99.9")
83
ReportLostMessage()
TimeoutMsgLost()
102
Message("99.9")
100
TimeoutMsgLate()
101
Message("999.9")
99
Command()
104
NoHandler()
Command()
106
Timeout()
Figure 6.10. Reactive system: interactive exploration showing path to unsafe state.
Liveness analysis depends on writing an accepting state condition that expresses
the goal we intend the program to achieve. An accepting state is often defined to be
a state where the program is allowed to stop. However, many programs including
embedded controllers (like the one in this example) are never supposed to stop. In
order to use liveness analysis with such systems, we must broadenour definition.We
110 Exploring and Analyzing Finite Model Programs
[AcceptingStateCondition]
public static bool SafeCalibrateEnabled()
{
return (CalibrateEnabled()
&& buffer == InRange
&& previous == double.Parse(InRange));
}
Figure 6.11. Reactive system: accepting state condition for liveness analysis.
now say that an accepting state is a state where a program goal has been achieved,
where some unit of work has been finished, where there is not a portion of work
left undone, where a task has been completed, and where there is not some task left
unfinished.
Pages:
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168