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

4MvingintoCode
Before moving from the formal specification into the verified code, we ought to
decide which methods we will use. A first way to proceed with the challenge is
to run the resulting code in an 8-bit PIC micro controller made available by the
Software Quality Research Laboratory, at the McMaster University (Canada).
That board was specifically designed to support the pacemaker functionalities.
However, due to budget restrictions we were not able to acquire that hardware
from McMaster University. Nevertheless, we still have other possible solutions to
simulate the verified code of the pacemaker. A first possible approach is to simu-
late the pacemaker on a Field Programmable Gate Array (FPGA). The strategy
is to refine the Z specification to pseudo-code using the Z Refinement Calcu-
lus [3] possibly with tool support [16], and then, use the pseudo-code to write
the program in languages like Handel-C [4] or SystemC [18], which are subsets of
C and C++ with features for describing hardware. By adopting this solution, we
would certainly spend a considerable amount of time refining the specification
and discharging proof obligations. Another approach to reach source code is to
translate our specification from Z to B using a tool like ProZ [19], an extension
of ProB. As an advantage, B has notably very good tools for refinement and
code generation such as Atelier-B and B-Toolkit, whose features are currently
lacking for the Z language. However, it is very likely that the resulting specifi-
cation would still require refinement within the B-Method. This would probably
yield the need for intervention in order to discharge the proof obligations gen-
erated, which normally takes a reasonable amount of time. Furthermore, the
modularisation of the Z specification might be compromised when translating
into B.
Our approach is to translate the Z specification into Perfect Developer, a soft-
ware produced by Escher Technologies, which provides fully automatic software
verification and code generation to languages like C, C#, and ADA. The Perfect
Developer language uses the notion of object orientation and can be easily learnt
by Z users since it has a syntax similar to the Z language. One of the similar-
ities between Z and Perfect Developer is the description of Z states in Perfect
Developer using classes. Within the class, variables, invariants and initialisation
are declared in separated sections. Moreover, schema operations in Z are trans-
lated into Perfect Developer in a similar fashion, except that preconditions and
postconditions are explicitly stated in separated sections.
The support guaranteed by Escher Technologies with quick answers and soft-
ware updates, allowing us to verify the entire specification of the pacemaker, was
yet another motivation for choosing Perfect Developer. The tool also has a very
good and automatic proof support. It automatically generates and discharges
all proofs that are necessary to verify the specification in order to guarantee the
consistency of the system. This means that Perfect Developer is able to verify,
for example, whether the state invariant is satisfied and if the preconditions of
each operation are satisfied. Some of these proofs have already been made in
ProofPower-Z in previous work, as discussed in [9], which required a consid-
erable amount of time. Hence, we have a tool that is capable of verifying our