Model-driven development is being used increasingly in the development of modern computer-based systems. In the case of cyberphysical 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.
CITATION STYLE
Woodcock, J., Foster, S., & Butterfield, A. (2016). Heterogeneous semantics and unifying theories. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9952 LNCS, pp. 374–394). Springer Verlag. https://doi.org/10.1007/978-3-319-47166-2_26
Mendeley helps you to discover research relevant for your work.