Biomedical Engineering Reference
In-Depth Information
Chapter 11
Conclusion
Abstract This chapter concludes the topic through summarising important points
of each chapter. The main contribution of this topic is to propose the formal meth-
ods based development life-cycle and associated techniques and tools, that are ex-
emplified by the grand challenge related to the cardiac pacemaker. Additionally, this
topic provides a technique for identifying anomalies in the standard ECG protocol
through incremental formalisation in Event-B.
11.1 Introduction
Highly critical systems, such as medical, avionic, and automotive systems require
high integrity, software reliability, and proof based development for complying with
certification standards [ 2 , 5 , 8 , 9 ], which evaluate the systems before their usage.
In this framework, adaptation of the formal method has become the state-of the-art
tech to meet the high demands on safety and reliability by certification bodies [ 6 ].
However, adaptation of formal methods significantly complicates the development
process of a system due to complexity of the modelling as well as a system itself.
Refinement based modelling techniques reduce verification effort significantly by
designing the whole system using the stepwise development process. The complete
system is verified with the help of theorem prover, model checker and animation
tools. Moreover, critical systems can be analysed already at the early stages of their
development, which allow to explore conceptual errors, ambiguities, requirement
correctness and design flaws before implementation of the actual system, and this
approach helps to correct errors more easily and with less cost.
This topic presents a new development life-cycle methodology, which is an ex-
tension of the waterfall model for developing the critical systems, where each phase
has used different kinds of techniques based on formal techniques. In current system
development process, formal methods are used only at the early stage of the system
development for verifying the requirements. We have proposed new development
methodology, which supports formal methods at every stage of the system devel-
opment process. We have not only used existing development life-cycle steps, but
also introduced some new steps in the life-cycle methodology. The proposed new
recursive approach is based on refinement techniques to build the whole system
from requirement analysis to code generation. New introduced techniques and tools
 
Search WWH ::




Custom Search