Formal Development of a Cardiac Pacemaker: From Specification to Code - Formal Methods: Foundations and Applications - page 222

OutputActualTime
Ξ PulseGenerator
out time !: int
out time != time
We were not able to translate those output operations to Perfect Developer
because we cannot describe precisely what is the effect of the output operation in
the executable code. For example, there is no way to precisely define whether the
output will be an output stream or a call to the operating system. The solution
is to translate those operations directly to the executable code, in our case, C#,
by creating an instance of the PulseGenerator class in which we develop those
methods equivalent to the output operations modelled in Z. In this way, we can
have those output operations, translated into C#, printing reports directly in
the graphical user interface developed by us.
7 Conclusions
In this paper we present our recent results in the formal development of a cardiac
pacemaker, one of the challenges in software verification suggested by the Verified
Software Initiative. Here, we provide a step forward from [9], where we present
our Z model and its verification using ProofPower-Z. In this paper, we describe
the approach used to encode the cardiac pacemaker based on the previously
presented Z model.
In a later stage, some possibilities for encoding the Z model have been consid-
ered and discussed in Section 4. A first possibility is to refine the Z model using
the Z Refinement Calculus. Although this would have a mechanical support, a
large amount of time would still be needed to discharge the proof obligations.
Another possibility is to translate the code into B by using ProB and then use
a B tool like Atelier-B to refine the specification to code mechanically. This ap-
proach, however, would still need some intervention since it would require further
refinement of the B model resulting from the translation. Finally, we discussed
the possibility to translate the Z model into Perfect Developer in order to get
an automatic code generation of the verified specification.
We have analysed the tool support for the refinement of the Z specification
into code and concluded that Perfect Developer could be a good way for this
purpose, since it provides an automatic generation of verified code and has an
excellent professional support team. This approach proved to be much easier than
refining the Z specification using the Z refinement calculus, as mentioned in [9],
which lacks stable tool support yielding to a need for handcrafted refinement and
proofs. However, we do not provide a formalisation and proof of the translation
from Z into Perfect Developer, which is left as an interesting piece of future work.
Currently, we rely on the fact that the translation from Z into Perfect Developer
is fairly direct.
This case study proved to be a complex task since the informal specifica-
tion [13] does not provide enough information for a software development team