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

formal specification with automatic proofs and also capable of a fully automatic
refinement of that specification into a source code that meets its requirements.
It means that we can avoid errors during the refinement process resulting in a
code without errors fully automatically. In the the next section, we present the
translation of our Z specification of the pacemaker to Perfect Developer.
5 From Z to Perfect Developer
The migration from Z into Perfect Developer is relatively straightforward due to
their similarity. The main idea is to translate a Z state as a Perfect Developer
class which will be refined to a Java or a C# class. A class in Perfect Developer
has a basic structure: all the variables and its types are declared in the abstract
section; the state invariants are declared in the invariant ;inthe interface we
include all components like functions, schemas and properties which will be
available (visible) to derived classes; in the build function we define which of the
variables of the state will have their initial values declared, which will be refined
to the constructor of the class in Java, for example. The Z schema operations
over the state are modelled very similarly in Perfect Developer except that they
are part of their related class. Moreover, the preconditions and postconditions
of a schema operation are separated into pre and post in Perfect Developer,
differently from Z where they are mixed in the same predicate. This normally
requires a pre-condition calculation, which we have done using ProofPower-Z.
However, despite being a complex system, the pacemaker pre-conditions were
fairly simple to calculate.
The pacemaker proved to be an interesting challenge not only because of the
complexity of its requirements, but also because of the complexity of its state
and operations, which are modelled using a large number of variables and op-
erations. In order to deal with this complexity, we adopted some methodologies
and patterns while programming. This helped us to generate a more compre-
hensible code. Furthermore, a later formalisation of these patterns fosters the
automation of such translation, which would allow a direct code generation from
ZusingPerfectDeveloperasameanstoachievethat.
One such pattern is to create schema operations to update the values of the
variables in a class, providing encapsulation of these variables. This makes it
unnecessary to redeclare the same variable as an interface of each derived class.
The pattern is as follows: for each variable included in the interface section,
we create a schema operation, prefixed by chg followed by the name of the
variable. In each schema operation, we can change only the value of that variable.
Moreover, unless the variables are included in the state invariants, there is no
precondition for the schema.
For example, for the TimeSt Z component, we create a class in Perfect Devel-
oper named TimeSt , in which we include the same variables as presented in the
Zmodelinthe abstract section. In this case, there is no state invariant in the
TimeSt Z component; hence, it is not necessary to include the invariant section.
By omitting the invariant section, Perfect Developer will assume that there is
no state invariant in the class.