© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Refining industrial scale systems in circus
M V M Oliveira, A L C Cavalcanti, and J C P Woodcock
In I.R. East, J. Martin, P.H. Welch, D. Duce, and M. Green, editors, Communicating Process Architectures 2004, volume 62 of Concurrent Systems Engineering Series, pages 182-196. IOS Press, September 2004.Abstract
Circus is a new notation that may be used to specify both data and behaviour aspects of a system, and has an associated refinement calculus. Although a few case studies are already available in the literature, the industrial fire control system presented in this paper is, as far as we know, the largest case study on the Circus refinement strategy. We describe the refinement and present some new laws that were needed. Our case study makes extensive use of mutual recursion; a simplified notation for specifying such systems and proving their refinements is proposed here.
Bibtex Record
@inproceedings{1949,
author = {M V M Oliveira and A L C Cavalcanti and J C P Woodcock},
title = {Refining Industrial Scale Systems in Circus},
month = {September},
year = {2004},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2004/1949},
publication_type = {inproceedings},
submission_id = {10687_1093006087},
ISBN = {1 58603 458 8 },
booktitle = {Communicating Process Architectures 2004},
editor = {I.R. East and J. Martin and P.H. Welch and D. Duce and M. Green },
volume = {62 },
series = {Concurrent Systems Engineering Series},
publisher = {IOS Press},
}