Information Technology Reference
In-Depth Information
since an integer may take more than these two values we can formalize this
restriction by formulating a user-defined predicate with this constraint as
follows:
//@ predicate true_or_false(int a) = (a == FALSE)||(a == TRUE);
The type invariant for
Vigilance_device
can be expressed by the pred-
icate
vigilance_invariant
as shown below. It is required that the status
may only be true or false as it's a Boolean value. Therefore, we use our for-
merly defined predicate
true_or_false
. Furthermore, there exists an equiv-
alence between the status of the buttons and the start and end time of their
invocation. If, and only if, the moment of releasing a button or pedal is after
it was pushed last time the value of the status is true.
/
*
@
predicate vigilance_invariant{L}(Vigilance_device
*
vig) =
true_or_false(vig->button_status) &&
(vig->button_status <==> vig->button_end_time < vig->button_start_time);
*
/
Similarly, we can also formulate a type invariant for the user-defined data
type
Locomotive
.
Below we can see an example of a predicate that checks whether the limit
for holding a vigilance pedal or button has expired. Due to the informal
specification this predicate remains true if any vigilance pedal or button
is currently invoked (
status
must be true) and the difference between the
actual time and the moment the button invocation was started exceeds thirty-
five sec., represented by
MAX_VIGILANCE_BUTTON_HOLD
.
/
*
@
predicate vig_button_hold_expired{L}
(Vigilance_device
*
vig, Locomotive
*
loc) = vig->button_status &&
(loc->actual_time - vig->button_start_time > MAX_VIGILANCE_BUTTON_HOLD);
*
/
Similarly, we can formulate a predicate that checks whether the pause
limit between the invocation of any vigilance pedal or button has expired.
The function
process_vigilance_device
checks whether the vigilance
device is processed correctly, which means, the vigilance buttons or pedals
are neither held nor paused too long. We can see the function contract for
such a function below.
/
*
@
requires \valid(vig) && \valid(loc);
requires locomotive_invariant(loc) && vigilance_invariant(vig);
requires actual_time_is_latest_time(vig, loc);
ensures locomotive_invariant(loc) && vigilance_invariant(vig);
ensures actual_time_is_latest_time(vig, loc);
behavior forced_brake_initiate:
assumes !loc->standstill &&
(vig_button_hold_expired(vig, loc) || vig_button_break_expired(vig, loc));
assigns loc->forced_brake && loc->train_brake;
ensures loc->forced_brake && loc->train_brake;
