By the same authors

Compositional Assume-Guarantee Reasoning of Control Law Diagrams Using UTP

Research output: Chapter in Book/Report/Conference proceedingChapter

Author(s)

Department/unit(s)

Publication details

Title of host publicationFrom Astrophysics to Unconventional Computation
DatePublished - 30 May 2019
Pages215-254
Number of pages40
PublisherSpringer
Original languageEnglish
ISBN (Electronic)978-3-030-15792-0
ISBN (Print) 978-3-030-15791-3

Abstract

Simulink is widely accepted in industry for model-based designs. Verification of Simulink diagrams against contracts or implementations has attracted the attention of many researchers. We present a compositional assume-guarantee reasoning framework to provide a purely relational mathematical semantics for discrete-time Simulink diagrams, and then to verify the diagrams against the contracts in the same semantics in UTP. We define semantics for individual blocks and composition operators, and develop a set of calculation laws (based on the equational theory) to facilitate automated proof. An industrial safety-critical model is verified using our approach. Furthermore, all these definitions, laws, and verification of the case study are mechanised in Isabelle/UTP, an implementation of UTP in Isabelle/HOL.

Discover related content

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

View graph of relations