Real-Time Animator and Requirements Traceability - Using Event-B for Critical Device Software Systems - page 89

confidence medical device [ 29 , 30 , 52 ] that is implemented to provide proper heart
rhythm when the body's natural pacemaker does not function properly. In the devel-
opment of the cardiac pacemaker, real-time animator of formal specification helps
to animate the formal model with a real-time data set instead of toy-data , and offers
a simple way for specifiers to build a domain-specific visualisation that can be used
by domain experts to check whether a formal specification corresponds to their ex-
pectations. The pacemaker models are validated to make sure that they meet all the
functional requirements of the cardiac pacemaker. The validation process is carried
out by both logic experts and medical experts.
5.7 Limitations
The proposed architecture of the real-time animator is sufficient to validate
refinement-based formal specifications using real-time data set instead of toy-data
set. The major limitation of this tool is real-time data collection and features extrac-
tion for testing the validation of formal specifications of a system, where feature
extraction algorithms are not able to calculate required features under real-time (i.e.
ECG features extraction). Due to limitation of this algorithm, we proposed off-line
validation technique using database. Database is used to store the extracted features
in a specific file format for validating the formal models.
Another limitation we have discovered through our experiments that every re-
finement step is not animatable, specially early development of the formal model
(or abstract model), where concrete functional behaviours of the system are not
specified yet. Incremental refinement approach builds the system gradually and pro-
vides the concrete system behaviour, which may be animatable. Refinement based
modelling helps for obtaining stepwise validation for modelling a system [ 38 ]. This
is consistent with using animation as a kind of quality-assurance activity during de-
velopment. Early stages of system models are too abstract and not able to present
parametric based desired behaviour of the system. So that, this real-time anima-
tion is useful to validate later refinement stages of a system or concrete models,
when some parametric behaviours are introduced in the system. These parameters
are used as features in the formal specifications for real-time validation. We believe
that one animation per abstraction level is sufficient. In fact, the first refinement of
a level may often have a non-determinism too wide to allow for meaningful ani-
mation (concept introduction), but subsequent refinements get the definitions of the
new concept precise enough to allow animation.
5.8 Summary
The objective of this proposed architecture is to validate the formal model with real-
time data set in the early stage of development without generating the source code
in any target language. Here, we focused the attention on the techniques introduced