By the same authors

Compositional Assume-Guarantee Reasoning of Control Law Diagrams using UTP

Research output: Working paper



Publication details

DateUnpublished - Apr 2018
Number of pages202
Original languageEnglish


This report is a summary of our work for the VeTSS funded project “Mechanised Assume-Guarantee Reasoning for Control Law Diagrams via Circus”. Our Assume-Guarantee (AG) reasoning of control law diagrams is based on Hoare and He’s Unifying Theories of Programming and their theory of designs. In this report, we present developed theories and laws to map discrete-time Simulink block diagrams to designs in UTP, calculate assumptions and guarantees, and verify properties for modelled systems. A practical application of our AG reasoning to an aircraft cabin pressure control subsystem is also presented. In addition, all mechanised theories in Isabelle/UTP are attached in Appendices. In the end of this report, we summarise current progress for each work package.

    Research areas

  • UTP, Simulink, Formal Verification, Isabelle/UTP, Assume-Guarantee, Contract-based Verification


Discover related content

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

View graph of relations