Tool Support for the CircusRefinement Calculus

Abstract

Circus combine both data and behavioural aspects of concurrent systems using a combination of CSP, Z, and Dijkstra’s command language. Its associated refinement theory and calculus distinguishes itself from other such combinations. Using a refinement calculus, we can correctly construct programs in a stepwise fashion. Each step is justified by the application of a refinement law, possibly with the discharge of proof obligations (hereafter called POs). The manual application of the refinement calculus, however, is an error-prone and hard task.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{GurgelCO08,
  author       = {Alessandro Cavalcante Gurgel and
                  Cristiano Gurgel de Castro and
                  Marcel Vin{\'{\i}}cius Medeiros Oliveira},
  editor       = {Egon B{\"{o}}rger and
                  Michael J. Butler and
                  Jonathan P. Bowen and
                  Paul Boca},
  title        = {Tool Support for the CircusRefinement Calculus},
  booktitle    = {Abstract State Machines, {B} and Z, First International Conference,
                  {ABZ} 2008, London, UK, September 16-18, 2008. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {5238},
  pages        = {349},
  publisher    = {Springer},
  year         = {2008},
  url          = {https://doi.org/10.1007/978-3-540-87603-8\_37},
  doi          = {10.1007/978-3-540-87603-8\_37},
  timestamp    = {Tue, 14 May 2019 10:00:50 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/GurgelCO08.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}