A Refinement Calculus for Circus - Mini-thesis

Most software developments do not use any of the existing theories and formalisms. This leads to a loss of precision and correctness on the resulting softwares. Two different approaches to formal techniques have been raised in the past decades: one focus on data aspects, and the other focus on the behavioural aspects of the system. Some combined languages have already been proposed to bring these two schools together. However, as far as we know, none of them has a related refinement calculus. Using Circus as the specification language, we can describe both data and control behaviour. The objective of this work is to formalise a refinement calculus for Circus. A refinement strategy for Circus, new refinement laws and their proofs are presented. The proofs are based on an extension of the existing Circus semantics, which is based on the unifying theory of programming. This extension, and its mechanisation, and the proof of the laws on ProofPower are also part of this work. We intend to provide a tool that supports the Circus refinement calculus. Furthermore, as an extension of the existing refinement strategy for Circus, we present a translation strategy for Circus programs. This translation strategy can be used as a guideline in the translation of Circus programs to Java. Furthermore, the mechanisation of this translation is also feasible. We present a case study, a safety-critical fire protection system, that, as far as we know, is the largest case study on the Circus refinement calculus. We present the refinement of its abstract centralised specification to a concrete distributed one. Finally, the translation of the concrete specification of the system to Java, using our translation strategy, is also presented. Throughout this mini-thesis, some sections, and even chapters are not written. They have not been removed from the mini-thesis on purpose. Our intention is to give an idea of the scope and the structure of our final thesis, which is discussed in details in the final chapter of this document.