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

this period, software have been delivered with restricted warranties of failures and
errors, resulting in the well-known software crisis. Due to software crisis, various
formalisms and rigorous techniques (VDM, Z, Event-B, Alloy, etc.) have been used
in the development process of safety-critical systems. These approaches provide a
given level of reliability and confidence to develop the error-free systems. Formal
methods and their tools have achieved some usability that could be applied even in
industrial-scale applications allowing software developers to provide more mean-
ingful guarantees to their projects.
Tony Hoare suggested Grand challenge for Computing Research [ 24 ] to inte-
grate the research community to work together towards a common goal, agreed to
be valuable and achievable by a team effort within a predicted time-scale. Verifi-
cation Grand Challenge is one of them. From the Verification, Grand Challenges,
many application areas were proposed by the Verified Software Initiative [ 25 ]. The
pacemaker specification [ 7 , 18 ] has been proposed by the software quality research
laboratory at McMaster University as a pilot project for the Verified Software Initia-
tive [ 38 , 59 ]. The challenge is characterised by system aspects including hardware
requirements and safety issues. Such a system demands high integrity to achieve
safety requirements. The pacemaker device is highly sensitive, and lots of operating
defects are coming day by day.
The contribution of this chapter is to give a complete idea of formal develop-
ment of the cardiac pacemaker using our proposed framework and a set of tech-
niques and tools. The cardiac pacemaker is a critical system, which is used here
to show the usefulness of proposed approaches. Our approach is based on the
Event-B modelling language which is supported by the Rodin platform integrat-
ing tools for proving models and refinements of models. Here, we present an in-
cremental proof-based development to model and verify such interdisciplinary re-
quirements in Event-B [ 1 , 8 ]. Validation of the system is done by model checker as
well as the real-time animator. The model checker, ProB tool [ 36 ]isusedforval-
idating and analysing the developed formal specifications. The cardiac pacemaker
models must be validated to ensure that they meet requirements of the pacemaker.
Hence, validation must be carried out by both formal modelling and domain ex-
perts. The real-time animator helps to the medical experts to verify the functional
behaviour of the system. If medical experts are not agreed on the system behaviour,
then the system specification is modified and again verify it. In addition, we have
proposed the system integration approach using refinements charts to help a code
designer to improve the code structure and code optimisation, and the code gen-
eration for synthesising and synchronising the software codes of the cardiac pace-
maker. We have also used our proposed environment model of the heart to specify
a closed-loop system of the heart and cardiac pacemaker. Finally, we have used
our translator (EB2ALL) [ 13 , 41 , 45 - 47 , 51 ] to generate the source code in mul-
tiple languages (C, C++, Java, C#). In the rest of the sections of this chapter, we
describe step by step a development of the one- and two-electrode cardiac pace-
maker.