By the same authors

Heterogeneous Semantics and Unifying Theories

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



Publication details

Title of host publication7th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation
DateAccepted/In press - 2016
Number of pages21
Original languageEnglish
ISBN (Electronic)978-3-319-47166-2


Model-driven development is being used increasingly in the development of modern computer-based systems. In the case of cyber-physical systems (including robotics and autonomous systems) no single modelling solution is adequate to cover all aspects of a system, such as discrete control, continuous dynamics, and communication networking. Instead, a heterogeneous modelling solution must be adopted. We propose a theory engineering technique involving Isabelle/HOL and Hoare & He’s Unifying Theories of Programming. We illustrate this approach with mechanised theories for building a contractual theory of sequential programming, a theory of pointer-based programs, and the reactive theory underpinning CSP’s process algebra. Galois connections provide the mechanism for linking these theories.

Discover related content

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

View graph of relations