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

In this section, we presented a brief overview of the translation from the Z
specification of the pacemaker into Perfect Developer.Basedonthistranslation,
we were able to automatically generate C# code and execute a simulation of the
pacemaker using a graphical user interface. In the next section, we provide an
analysis of the results we have achieved.
6 Analysis of Results
Our decision to adopt Perfect Developer was based on the similarities to the Z
language like the use of state invariants and operations as schemas. Furthermore,
the possibility to automatically generate verified code was also an attractive
factor in our choice. Throughout the development process we had a very good
support from the software vendors, who helped us to solve issues during the
translation to the new syntax and even removed some of the limitations of the
software's free version.
The translation from Z to Perfect Developer required some adaptations of our
specification to the syntax of the latter. Some of those adaptations have been
presented in this current paper, like the use of classes to model components and
the PulseGenerator itself, and the instantiation of each component as a member
of the system state. Besides, we had to explicitly state the preconditions and
postconditions that are not separated in Z. We have also translated the remaining
operations, those related to the tests made by the pacemaker, where it generates
reports of events occurred during the therapy.
In a first version of the translation into Perfect Developer, we generated over
3360 lines of code; the PulseGerator class alone contained 1300 lines of code. The
generation resulted in over 740 proof obligations that were automatically proved
by the Perfect Developer theorem prover. Using an Intel Core2 Duo 2.4 Ghz with
3Gb DDR2 RAM machine, all proofs were discharged in less than 5 minutes. This
version reached 116% of Perfect Developers Academic license capacity, which is
based on the number of source code tokens parsed. For this reason, a specific
version was provided to us by Escher Technologies, which allowed us to conclude
the whole development.
Following a suggestion from the Perfect Developer support team, we devel-
oped a second version of the system. Based on their suggestion, we made some
modifications in the code by moving the preconditions of the schema operations
of PulseGenerator class to boolean functions, allowing their reuse in other opera-
tions. For instance, the PulseGenerator class was reduced from 1300 to 750 lines
of code. As a consequence, the number of proof obligations was also reduced
to around 560. The overall time spent for discharging proofs was 86 seconds,
since most of the proofs required less than one second to be discharged. Thus,
this change considerably reduced the size of the generated executable code to
an amount of 9585 lines of code. This version reached almost 65% of Perfect
Developers Academic license capacity.
The work presented in this paper is a significant development of the work
presented in [9]. First, we were able to verify the entire version of our Z model