Formal Derivation of State-Rich Reactive Programs using Circus

The lack of formalism in most software developments can lead to a loss of precision and correctness in the resulting software. Formal techniques of program development have been developed in the past decades and can tackle this problem. Two different approaches have been taken: one focuses on data aspects, and the other focuses on behavioural aspects of the systems. Some combined languages have already been proposed to integrate these two approaches; however, as far as we know, none of them, apart from Circus, includes a refinement calculus.

This work presents a method that can be applied in order to achieve a formal derivation of state-rich reactive programs, using Circus, in a calculational style. It extends the existing Circus refinement strategy to reach Java implementation and formalises its refinement calculus. For that we proposed and mechanised a denotational semantics for Circus, which was used to prove over one-hundred and forty refinement laws, many of which were suggested by an industrial case study on which we worked. As far as we know, this is the only mechanised semantics for languages like Circus; the mechanisation of the Circus semantics and its theoretical basis, the Unifying Theories of Programming, are the basis for a theorem prover for Circus. A translation strategy from Circus to Java is also an important part of this work.

Our method is illustrated by the case study: a safety-critical fire protection system. So far, this is the largest case study on the Circus refinement calculus. We present the refinement of its abstract centralised specification to a concrete distributed one, and then its translation to Java, using our translation strategy. We believe that this industrial-scale case study provides empirical evidence that the formal development of state-rich reactive processes using Circus is possible in both theory and practice.


TECHNICAL NOTICE: In order to be able to see the menu of documents to the left of this page, you may need to allow this page to show active contents. Alternatively, click here, for a page with a static menu.