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

methodology uses only refinement approach to build the complete system and each
refinement level is verified using different techniques. Last level of the system is
the concrete model, which has been used for producing the source code. The code
generation tool EB2ALL is very simple in use, which can generate the optimised
codes for future use. The process for system development is user friendly, but a
developer has required the strong knowledge of formalisation and refinement tech-
niques to build the correct system using this new system development methodology
and associated techniques and tools.
9.15 Summary
In this chapter, we have presented the pacemaker specification, one of the chal-
lenges proposed by the Verified Software Initiative [ 25 ]. We have developed the
formal model of the pacemaker system in Event-B and discovered the exact func-
tional behaviour of the pacing and sensing events. Our approach for formalising
and reasoning about action-reaction is based on real-time as a pacemaker system.
The pacemaker case study suggests that such an approach can yield a viable model
that can be subjected to useful validation against system-level properties at the early
stage of the development process. The proposed techniques based on development
patterns intend to assist in the design process of the system where correctness and
safety are important issues.
A series of high confidence medical devices of increasing scope and complex-
ity will follow the pacemaker system. Main advantage of proposed development
methodology and a set of associated techniques and tools is the ability to develop
the whole system from requirement analysis to code generation. Proposed method-
ology exploits the advance capabilities of the combined approach of formal verifi-
cation and model validation using a model-checker, use of real time animation to
test system behaviour and, finally automatic source code generation from a verified
formal model in order to achieve the considerable advantages for a critical system
design.
The proposed approach has also involved the use of the real-time animator for
executing formal specification to validate the actual requirements. The main objec-
tives of this real-time animator [ 42 ] are to promote the use of such kinds of tool to
bridge a gap between software engineers and stakeholders to build quality system
and to discover all the ambiguous information from the requirements. Moreover,
this tool helps to verify the correctness of behaviour of the system according to the
stakeholders requirements. The combined approach of the formal verification and
real-time animation allows the systematic development of a clear, concise, precise
and unambiguous specification of a software system and enables to the software en-
gineers to animate the formal specification at the early stage of the development. The
formal specification animation is supported by both software engineers and stake-
holders. Our case study on cardiac pacemaker illustrates the potential value which is
a formal specification, and its subsequent animation can bring to the comprehension
and clarification of the informal requirements.