Paper Info
Title
A UTP semantics for Circus
Abstract
Circus specifications define both data and behavioural aspects of systems using a combination of Z and CSP constructs. Previously, a denotational semantics has been given to Circus; however, a shallow embedding of Circus in Z, in which the mapping from Circus constructs to their semantic representation as a Z specification, with yet another language being used as a meta-language, was not useful for proving properties like the refinement laws that justify the distinguishing development technique associated with Circus. This work presents a final reference for the Circus denotational semantics based on Hoare and He’s Unifying Theories of Programming (UTP); as such, it allows the proof of meta-theorems about Circus including the refinement laws in which we are interested. Its correspondence with the CSP semantics is illustrated with some examples. We also discuss the library of lemmas and theorems used in the proofs of the refinement laws. Finally, we give an account of the mechanisation of the Circus semantics and of the mechanical proofs of the refinement laws.
Year
DOI
Venue
2009
10.1007/s00165-007-0052-5
Formal Asp. Comput.
Keywords
Field
DocType
z specification,refinement law,circus denotational semantics,reflnement calculus,csp semantics,circus semantics,csp construct,theorem proving,utp semantics,circus construct,circus specification,denotational semantics,refinement calculus,concurrency,behavioural aspect,theorem proving.,relational model
Specification language,Programming language,Refinement calculus,Computer science,Concurrency,Denotational semantics,Automated theorem proving,Theoretical computer science,Mathematical proof,Relational model,Semantics
Journal
Volume
Issue
ISSN
21
1-2
1433-299X
Citations 
PageRank 
References 
50
1.71
25
Authors
3
Name
Order
Citations
PageRank
Marcel Oliveira117212.57
Ana Cavalcanti21407.68
Jim Woodcock335725.74