Biomedical Engineering Reference
In-Depth Information
cardiac pacemaker formal model into 'C' using EB2C tool. Based on this transla-
tion, we were able to automatically generate 'C' code and execute a simulation of
the pacemaker.
9.14 Discussion
New development methodology is successfully applied for developing the cardiac
pacemaker from requirement analysis to code implementation. The whole system
development life-cycle is based on formal techniques. The complete system is de-
signed using different kinds of tools related to the formal techniques. The Event-B
modelling language is used for formalising the pacemaker system using refinement
techniques. Each level of refinements is validated through the ProB model checker
and the real-time animator for verifying the correctness of the system behaviours
against requirements and according to the medical experts, respectively. If any er-
ror is discovered during verification, validation or domain experts reviews, then the
pacemaker specification is modified and again follow the verification, validation and
domain experts reviews. This process is continued applied in a loop until not find
the correct proved formal specification of the cardiac pacemaker. The verification,
validation and domains experts reviews are applied on each refinement level for
modelling the whole system. To handle the complexity of a system according to the
refinements, we have used the refinement chart to model the cardiac pacemaker sys-
tem. The refinement charts of the pacemaker present integration architecture of the
system in form of all possible operating modes. Some operating modes are an ex-
tension of the existing operating modes, it is clearly expressible from the refinement
charts. This technique is not only for code integration, but also it helps for analysing
the operating modes and code structuring of the system. Finally, we have used the
tool EB2ALL for generating the source code into multiple languages (C, C++, C#,
and Java) from the formal specifications. In this development process, we have not
considered the safety assessment approach.
According to the existing development life cycle, we use formal methods only on
the selected part of the system for verifying the correctness of the system against re-
quirement. No formal methods are likely to be suitable for describing and analysing
every aspect of a complex system; a practical approach is to use different meth-
ods in combination. In this topic, we have provided some possible solutions for
emerging problems in area of software engineering related to the development of
critical systems, where we have proposed a development life-cycle and associated
a set of techniques and tools to develop the highly critical systems using formal
techniques from requirements analysis to automatic source code generation. There
is not a set of supporting tools, which can be used for system development using
only formal techniques. We have developed a set of new tools, which support a rig-
orous framework for the system development and finally; we have applied this new
development life-cycle methodology and associated tools for developing the car-
diac pacemaker system for assessing the usability of our proposed approach. This
Search WWH ::
Custom Search