Compositional Assume-Guarantee Reasoning of Control Law Diagrams Using UTP

Research output: Chapter in Book/Report/Conference proceedingChapter


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.
Original languageEnglish
Title of host publicationFrom Astrophysics to Unconventional Computation
Number of pages40
ISBN (Electronic)978-3-030-15792-0
ISBN (Print) 978-3-030-15791-3
Publication statusPublished - 30 May 2019

Cite this