Paper Details

Communicating Process Architectures (CPA)
 Title: The COMPASS Modelling Language: Timed Semantics in UTPĀ 
 Conference: Communicating Process Architectures 2014
 Authors: Jim Woodcocka, Jeremy Bryansb, Samuel Canhama, Simon Fostera
(a) Department of Computer Science, University of York
(b) School of Computing Science, Newcastle University
 Abstract: We describe the denotational semantics of a subset of the COMPASS Modelling Language (CML), using Hoare & He's Unifying Theories of Programming. The subset consists of rich state and operations based on VDM, concurrency and communication, based on CSP, and discrete time, based on Timed CSP. Other features of CML not treated here include object orientation, pointers and object references, and mobile processes and channels; extensions planned for the future include priority, probabilistic choice, and continuous time. A rich collection of language features such as this presents significant challenges when building a formal semantics, so the approach taken in CML is compositional: each feature is given a separate semantics and a domain-specific language is then composed from whichever features are required for the job in hand. Composition is achieved from the use of Galois connections. In this paper, we describe the semantics for the timed, imperative process algebra subset of CML. We adopt a semantic domain suggested by Lowe & Ouaknine — timed testing traces — as the basis for our UTP semantics. We include an example CML specification taken from industry: a leadership election protocol for a system of systems. 

BibTeX Entry

Full paper