Compositional Assume-Guarantee Reasoning of Control Law Diagrams Using UTP
Research output: Chapter in Book/Report/Conference proceeding › Chapter
Title of host publication | From Astrophysics to Unconventional Computation |
---|
Date | Published - 30 May 2019 |
---|
Pages | 215-254 |
---|
Number of pages | 40 |
---|
Publisher | Springer |
---|
Original language | English |
---|
ISBN (Electronic) | 978-3-030-15792-0 |
---|
ISBN (Print) | 978-3-030-15791-3 |
---|
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