The Cardiac Pacemaker - Using Event-B for Critical Device Software Systems - page 215

A new event ( Acler_sensed ) is defined as to simulate the behaviour of the ac-
celerometer sensor. This event is continued sensing the motion of the body to in-
crease or decrease the length of the pace interval ( Pace_Int ). In this event, the guards
state that the accelerometer sensor flag is TRUE and the hysteresis state is FALSE.
A new variable acl_sen is used to store the current sensing value. The actions of
this event state that the local variable acl_sen updates the accelerometer sensor
( acler_sensed ) and the accelerometer sensor flag ( acler_sensed_flag ) sets FALSE.

EVENT Acler_sensed
ANY
acl _ sen
WHERE
grd1 : acl _ sen ∈ N

grd1 : acler _ sensed _ flag = TRUE

grd1 : HYT _ State = FA L S E

THEN

act1 : acler _ sensed := acl _ sen

act1 : acler _ sensed _ flag := FA L S E

END

Finally, we have completed the formal specifications of the one- and two-
electrode cardiac pacemaker. The next section describes the validation of the formal
model using ProB animator.

9.9 Model Validation and Analysis

There are two main validation activities in Event-B, and both are complementary
for designing a consistent system:

• Consistency checking , which is used to show that the events of a machine preserve

the invariant, and refinement checking , which is used to show that one machine is
a valid refinement of another. A list of automatically generated proof obligations
should be discharged by the proof tool of the Rodin platform.

• Model analysis , which is done by the ProB tool and consists in exploring traces or

scenarios of our consistent Event-B models. For instance, the ProB may discover
possible deadlocks or hidden properties that are not expressed by generated proof
obligations.

This section conveys the validity of the model by using ProB tool [ 36 ] and Proof
Statistics. “Validation” refers to the activity of gaining confidence that the devel-
oped formal models are consistent with the requirements, which expressed in the
requirements document [ 7 ]. We have used the ProB tool [ 36 ] that supports au-
tomated consistency checking of Event-B machines via model checking [ 10 ] and
constraint-based checking [ 28 ]. Animation using ProB worked very well, and we
have then used ProB to validate the Event-B machine. This tool assists us to find