Automating Refinement of Circus Programs - Formal Methods: Foundations and Applications - page 286

5 Practical Experiences

The primary motivation for the treatment of well-definedness in the last two
sections is the automation of complex refinement strategies using our tools and
the semantic embedding of . As a case study, we have automated part of

the refinement strategy for control laws described in [2,3].
The work in [2,3] describes first how a formal account of (a subset of) the
Simulink notation can be given by translating the diagrams into

Circus

specifica-
tions. (Simulink is a de facto industry standard for the design of control systems.)
It then presents a strategy for refinement that gradually transforms the diagram
specification into a

Circus

Circus

model of a given Ada program, and thereby verifies
the correctness of the Ada implementation. For the encoding of the ArcAngel C
tactics, we refer to the work in [13]. The tactics we mechanise are mostly literal
translations of those in [13], including the various laws they rely upon.

The refinement strategy is structured into four phases, and so far we only
automated the first phase NB . This is itself subdivided into 7 steps, NBStep1
to NBStep7 , which are assembled into one compound tactic NBMain .Thetactic
deals with the normalisation of

Circus

processes representing blocks (or subsys-
tems) that are realised sequentially in code. Their model is given by a single
centralised process with two parallel actions. The tactic attempts to remove the
parallelism between these actions. A more detailed account of the refinement
strategy is omitted as it would take us too far from the agenda of the paper.
Our example specification is part of the model for the PID controller in [3].
In particular, we have applied the tactics to the model of a differentiator. It
is a simple example, which, however, as we discuss below, already reveals the
importance and effectiveness of our treatment of well-formedness.
Having encoded the tactics and laws, we have verified by inspection, that all
assumptions that remain after the application of the tactics are genuine proof
obligations. As explained in Section 4.2, particular kinds of provisos, namely
those resulting from μ , at present cannot be discharged automatically. We
verified, however, that these are the only residual provisos, apart from the well-
definedness assumption of the initial program of the refinement.
This initial analysis has uncovered some glitches in the recast theories and
implementation that have been subsequently fixed. One of them was a missing
wd axiom for one of the

Circus

operators which resulted in a simplification tactic
failing. As already mentioned, the implementation has been designed to robustly
deal with such cases, hence no error is raised when individual simplifications of
provisos do not succeed. (In some cases this leads to a partial proof encoded
as a 'reduced' proviso, and in other cases the proviso remains unchanged.) We
have increased the eciency of simplification tactics by incorporating guarding
conditions that ensure they are only applied to assumptions of the correct shape,
and furthermore only involve a predictably small number of proof steps.
We have also compared the eciency of our technique to that of the stan-
dard explicit treatment of provisos. Since our extensions to the ArcAngel C

Circus

im-
plementation are fully backward compatible, it is possible to revert to the old
shape of laws and model theorems and execute the same tactics under the same