Heterogeneous Semantics and Unifying Theories

Jim Woodcock; Simon David Foster; Andrew Butterfield

Heterogeneous Semantics and Unifying Theories

Jim Woodcock, Simon David Foster, Andrew Butterfield

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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 language	English
Title of host publication	7th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation
Pages	374-394
Number of pages	21
ISBN (Electronic)	978-3-319-47166-2
Publication status	Accepted/In press - 2016

Access to Document

ISoLA-SL-paperAccepted author manuscript, 480 KB

http://link.springer.com/chapter/10.1007%2F978-3-319-47166-2_26

Cite this

@inproceedings{e3e3da395bd04aba910df7c45d53bb16,

title = "Heterogeneous Semantics and Unifying Theories",

abstract = "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{\textquoteright}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{\textquoteright}s process algebra. Galois connections provide the mechanism for linking these theories.",

author = "Jim Woodcock and Foster, {Simon David} and Andrew Butterfield",

year = "2016",

language = "English",

isbn = "978-3-319-47165-5",

pages = "374--394",

booktitle = "7th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation",

}

TY - GEN

T1 - Heterogeneous Semantics and Unifying Theories

AU - Woodcock, Jim

AU - Foster, Simon David

AU - Butterfield, Andrew

PY - 2016

Y1 - 2016

N2 - 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.

AB - 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.

M3 - Conference contribution

SN - 978-3-319-47165-5

SP - 374

EP - 394

BT - 7th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation

ER -