VeTSS - Compositional Assume-Guarantee Reasoning of Control Law Diagrams using UTP (Oct 2017 - March 2018)

This project is funded by VeTSS (UK Research Institute in Verified Trustworthy Software Systems). In this project, we have developed a theoretical reasoning framework for discrete-time blocks of control law diagrams. The framework is based on Hoare and He’s Unifying Theories of Programming and their theory of designs. Using UTP to give denotational semantics to block diagrams generalises the framework and makes it easily be used for another block diagrams like Modelica, or other stream based languages. In addition, our framework supports reasoning of non-deterministic and non-input-receptive systems as well as systems with algebraic loops. Particularly, we use compositional reasoning and theorem proving to tackle the state space explosion problem.

In terms of outcomes, we developed

• a theoretical reasoning framework for the discrete-time part of control law block diagrams (such as Simulink) using theorem proving (based on the mathematical semantics of diagrams and capable of dealing with large state spaces)

it supports

• contract-based compositional reasoning (using refinement relation) to tackle verification of large systems

it is

• able to reason and resolve diagrams with algebraic loops (ignored by most verification approaches)

and we have

• verified one subsystem of an aircraft cabin pressure control application (from industry)

More information could be found in the technical report.