Conclusion - Using Event-B for Critical Device Software Systems - page 301

claims help to design an error-free system and different phases of the system have
been shown by refinements in form of formal development as well as refinement
charts. We have presented evidence that such an analysis is fruitful for both formal
and non-formal group of people. The second observation from our experiments is
that development of multiple models helped us not only find errors in the require-
ments documents but also gave us an opportunity to better understand intricate re-
quirements such as the control algorithm of a critical system. Moreover, we believe
that the effort needed is commensurate with the benefits we derive from developing
the multiple models.
In order to assess the overall utility of our approach, a selection of the results
of the formalisation and verification steps have been presented to a group of pace-
maker developers (French-Italian based pacemaker company). The developers are
satisfied by the result of pacemaker development using this methodology in sense
of incremental development as well as integration of hardware and software. They
really agreed on the refinement charts for showing operating mode relation and their
mode transitions. Throughout our case study, we have shown formal specification
and verification of the cardiac pacemaker system and the models must be validated
to ensure that they meet requirements. Hence, validation must be carried out by both
formal modelling and domain experts. Based on the experiment described above
and our conclusions we are convinced of the usefulness on certain areas, and there-
fore, we are considering to use this methodology for designing the highly critical
systems. The proposed framework and developed techniques and tools offer sys-
tem development from formal verification to code generation, which offer to obtain
that challenge of complying with FDA's QSR, ISO/IEC and IEEE standards quality
system directives [ 2 , 5 , 8 - 10 ] and help to get certification for the highly complex
critical systems.
11.5 Medical Protocol
This topic also contributes in the area of formal representation of the medical pro-
tocol. The formal model of medical protocol is verified, and this verified model is
not only feasible but also useful for improving the existing medical protocol. We
have fully formalised a real-world medical protocol (ECG interpretation) in an in-
cremental refinement-based formalisation process, and we have used proof tools to
systematically analyse whether the formalisation complies with certain medically
relevant protocol properties [ 20 , 23 ]. The formal verification process has discov-
ered a number of anomalies. We have also discovered a hierarchical structure for
the ECG interpretation efficiently that helps to discover a set of conditions that can
be very helpful to diagnose particular disease at early stage of the diagnosis without
using multiple diagnosis. Our hierarchical tree structure provides more concrete so-
lutions for the ECG interpretation protocol and helps to improve the original ECG
interpretation protocol. The main objective of this approach is to test correctness and
consistency of the medical protocol. This approach is not only for diagnosis purpose,