Heterogeneous Semantics and Unifying Theories

Jim Woodcock, Simon David Foster, Andrew Butterfield

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


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.
Original languageEnglish
Title of host publication7th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation
Number of pages21
ISBN (Electronic)978-3-319-47166-2
Publication statusAccepted/In press - 2016

Cite this