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

Automating Refinement of Circus Programs

Frank Zeyda and Ana Cavalcanti

University of York, Heslington, York, YO10 5DD, U.K.
{ zeyda,ana } @cs.york.ac.uk

Abstract. In previous work, we have presented a mechanisation of Cir-
cus for the theorem prover ProofPower-Z . Circus is a refinement language
for state-rich reactive systems that combines Z and CSP. In this paper,
we present techniques to automate the discharge of proof obligations typ-
ically generated by the Circus refinement laws. They eliminate most of the
proofs that are imposed by the fact that the encoding has to be precise
about typing and well-definedness issues, and leave just those that are
expected in a pen-and-paper refinement. This allows us to concentrate
on the proof of properties that are significant for the problem at hand,
while benefiting from the increased assurance and eciency afforded by
the use of a theorem prover as well as high-level tactic languages for
refinement. Our case study is a refinement strategy for verification of
control systems; we present the result of several experiments.

Keywords:

theorem proving, tactics, ArcAngel C , ProofPower .

1 Introduction

Circus [4] is a process algebra that captures stateaswellasbehavioural aspects

of a system. Its key concept is that of a process, which, like a CSP [15]

process, communicates with the environment via channels, but also aggregates
local state that can be internally accessed and modified. A

Circus

process spec-
ification contains a Z schema that specifies its state, and a list of dependent
local actions used by the process, of which a designated action, the main action,
defines the process behaviour. Actions may be specified using a mixture of CSP
constructs, Z operation schemas [16], and guarded commands of Dijkstra and
Morgan [5,8]. Processes can also be combined using CSP constructs.
A notable feature of the

Circus

language is its formal semantics and associated
refinement calculus [4]. This permits the derivation or verification of executable
programs. The flexibility of the language to handle both sequential behaviour
and parallelism in a unified way makes it especially suitable for the description
and formal derivation of state-rich concurrent systems [9].
A semantic embedding of

Circus

for ProofPower-Z , a theorem prover based
on HOL that also supports Z, was first presented in [12]. We have extended
that encoding to handle types and

Circus

Circus programs (rather than the Circus se-

mantics [19]). We have also developed a ProofPower implementation of

ArcAngel C [18]. This is a refinement-tactic language to formulate strategies to

automate the derivation and verification of programs from Circus specifications.