By the same authors

Engineering UToPiA - Formal Semantics for CML

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Published copy (DOI)



Publication details

Title of host publicationFM 2014: Formal Methods
DatePublished - 2014
EditorsCliff Jones, Pekka Pihlajasaari, Jun Sun
Original languageEnglish
ISBN (Print)978-3-319-06409-3

Publication series

NameLecture Notes in Computer Science


We describe the semantic domains for Compass Modelling Language (CML), using Hoare & He’s Unifying Theories of Programming (UTP). CML has been designed to specify, design, compose, simulate, verify, test, and validate industrial systems of systems. CML is a semantically heterogeneous language, with state-rich imperative constructs based on VDM, communication and concurrency based on CSP, object orientation with object references, and discrete time based on Timed CSP. A key objective is to be semantically open, allowing further paradigms to be added, such as process mobility, continuous physical models, and stochastic processes. Our semantics deals separately with each paradigm, composing them with Galois connections, leading to a natural contract language for all constructs in all paradigms. The result is a compositional formal definition of a complex language, with the individual parts being available for reuse in other language definitions. The work backs our claim that use of UTP scales up to industrial-strength languages: Unifying Theories of Programming in Action (UToPiA).

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations