By the same authors

Towards Verification of Cyber-Physical Systems with UTP and Isabelle/HOL

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

Author(s)

Department/unit(s)

Publication details

Title of host publicationConcurrency, Security, and Puzzles
DateAccepted/In press - 7 Nov 2016
DatePublished (current) - 9 Jan 2017
Pages39-64
Number of pages25
PublisherLecture Notes in Computer Science
Volume10160
Original languageEnglish
ISBN (Electronic)978-3-319-51046-0
ISBN (Print)978-3-319-51045-3

Abstract

In this paper, we outline our vision for building verification tools for Cyber-Physical Systems based on Hoare and He’s Unifying Theories of Programming (UTP) and interactive proof technology in Isabelle/HOL. We describe our mechanisation and explain some of the design decisions that we have taken to get a convenient and smooth implementation. In particular, we describe our use of lenses to encode state. We illustrate our work with an example UTP theory and describe the implementation of three foundational theories: designs, reactive processes, and the hybrid relational calculus. We conclude by reflecting on how tools are linked by unifying theories.

Bibliographical note

© 2017, Springer. Self-archiving of author accepted manuscript not supported by the publisher.

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations