Heterogeneous semantics and unifying theories

Jim Woodcock*, Simon Foster, Andrew Butterfield

*Corresponding author for this work

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

Abstract

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.

Original languageEnglish
Title of host publicationLeveraging Applications of Formal Methods, Verification and Validation
Subtitle of host publicationFoundational Techniques - 7th International Symposium, ISoLA 2016, Proceedings
EditorsTiziana Margaria, Bernhard Steffen
PublisherSpringer
Pages374-394
Number of pages21
ISBN (Print)9783319471655
DOIs
Publication statusPublished - 5 Oct 2016
Event7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016 - Imperial, Corfu, Greece
Duration: 10 Oct 201614 Oct 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9952 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016
Country/TerritoryGreece
CityImperial, Corfu
Period10/10/1614/10/16

Bibliographical note

Publisher Copyright:
© Springer International Publishing AG 2016.

Cite this