Information Technology Reference
In-Depth Information
2
Requirements Analysis
The vigilance device monitors the alertness of a train operator. Such a mecha-
nism must be introduced to detect whether a train operator has fallen asleep,
is ill, or possibly has died. While the train is in operation, the driver must
prove his/her attentiveness by invoking the vigilance device regularly. e.g., by
pushing a button. The informal requirements read: 1.) If the train operator
does not apply at least one of the vigilance device pedals or buttons within a
timed interval of eight seconds the forced brake must apply automatically. 2.)
If the train operator continuously applies at least one of the vigilance device
pedals or buttons for more than thirty-five seconds the forced brake must
apply automatically.
Figure 2 depicts the UML state diagram for the vigilance device described
above.
vigilance device deactivated
when standstill /
deactivate
when not standstill /
activate
vigilance device activated
push
waiting
to be
applied
after 35 s /
apply forced brake
applied
release
after 8 s /
apply forced brake
Fig. 2. UML State Diagram of a Vigilance Device.
Note that the state diagram is already more specific than the informal
specification since it introduces different states of the vigilance device. With
these states one can specify that no buttons need to be pushed while the
train is at standstill.
3
Subsystem Design and Formal Specification with
ACSL
For our case study we consider user-defined data types containing the core
data of the locomotive and the vigilance device. Figure 3 depicts the model
of the data structures
Locomotive
and
Vigilance_device
.
In
Locomotive
the variable
actual_time
represents a relative-time coun-
ter expressed in milliseconds (msecs). The variable
speed
measures the ve-
locity of the train in km/h. The variables
standstill
,
train_brake
and
