Figures 3.9??“3.11 display
portions of the FSM that show paths to interesting states. Each path through the
FSM is a possible run of the system. The FSM represents all possible runs of this
system. There are 121 states and 239 transitions between states. The model program
has to have some additional methods and variables (which do not appear in the
implementation) that represent the environment where the controller runs, including
the timer and sensor. Therefore, the actions in the diagrams include some that do not
appear in the controller implementation. For example, our implementation??™s Timeout
event must be represented here by Timeout, TimeoutMsgLate, and TimeoutMsgLost.
We also need a NoHandler action here to represent what happens when no handler
is enabled.
For safety analysis, the mpv tool searches for unsafe states where the controller
attempts to calculate the calibration factor when the temperature sample is
Overview 49
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.
Pages:
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91