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 language | English |
---|---|
Title of host publication | Leveraging Applications of Formal Methods, Verification and Validation |
Subtitle of host publication | Foundational Techniques - 7th International Symposium, ISoLA 2016, Proceedings |
Editors | Tiziana Margaria, Bernhard Steffen |
Publisher | Springer |
Pages | 374-394 |
Number of pages | 21 |
ISBN (Print) | 9783319471655 |
DOIs | |
Publication status | Published - 5 Oct 2016 |
Event | 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016 - Imperial, Corfu, Greece Duration: 10 Oct 2016 → 14 Oct 2016 |
Publication series
Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 9952 LNCS |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016 |
---|---|
Country/Territory | Greece |
City | Imperial, Corfu |
Period | 10/10/16 → 14/10/16 |
Bibliographical note
Publisher Copyright:© Springer International Publishing AG 2016.