Skip to main content
Kent Academic Repository

A Refinement Calculus for Circus - Mini-thesis

Oliveira, Marcel V. M. (2004) A Refinement Calculus for Circus - Mini-thesis. Technical report. University of Kent, Computing Laboratory, University of Kent, Canterbury, Kent, CT2 7NF, UK (KAR id:14175)

Abstract

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.

Item Type: Reports and Papers (Technical report)
Uncontrolled keywords: Concurrency; Z; CSP; Program Development
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Wheadon
Date Deposited: 24 Nov 2008 18:02 UTC
Last Modified: 16 Nov 2021 09:52 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/14175 (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.