PI: Jim Woodcock, Co-I: Simon Foster, University of York
- Theoretical reasoning framework for discrete-time part of control-law block diagrams (such asSimulink), based on mathematical semantics of diagrams and capable of dealing with large state spaces.
- Contract-based compositional reasoning using refinement for verification of large systems.
- Supports reasoning about diagrams with algebraic loops, ignored by most other verification approaches.
- Verification of a subsystem of an industrial aircraft cabin-pressure control application.
Control-law diagrams are used in industry to model complex engineering systems, such as the many components of modern aircrafts. These systems must be built to the very highest standards possible, and their control laws must be verified to ensure that they behave as required. Our project proposes a general methodology based on mathematical descriptions of diagrams. It is expressive enough both to capture the full range of behaviours required and to be used with other engineering techniques and their own diagrams and notations.
Our techniques scale up to tackle verification of large-scale systems. In this VeTSS-funded project, we developed a theoretical reasoning framework for discrete-time blocks of control-law diagrams. As well as giving a mathematical meaning to Simulink (an industry-standard diagrammatic notation for depicting control laws), our framework links to Modelica (another industry standard notation) for multi-model descriptions. Our verification technique relies on computer programs that automatically follow human patterns of reasoning.
We used our framework to verify the control laws for a subsystem used in aircrafts that controls the cabin pressure after landing. Specifically, the cabin-pressure system must keep working until the aircraft has made a successful landing and the cabin doors have been open for a minimum amount of time. The subsystem is made by Honeywell and we worked with colleagues at D-RisQ. Our technique revealed a vulnerable block that should be improved. The outcomes of this project include a theory to reason about block diagrams using mathematical contracts, mechanisation of the theory in the Isabelle theorem prover, as well as the verification of the cabin-pressure control subsystem. A technical report is available online.
PUBLICATIONS. K. Ye, S. Foster, J. Woodcock. “Compositional Assume-Guarantee Reasoning of Control-Law Diagrams using UTP”, From Astrophysics to Unconventional Computation, pp. 215-254, Springer International Publishing, 2020.
RELATED GRANTS. Dr Simon Foster, EPSRC UKRI Innovation Fellowship: “CyPhyAssure: Com-positional Safety Assurance for Cyber-Physical Systems”, £562,549, 06/2018–05/2021, with project partners ClearSy and D-RisQ.
IMPACT. “Simulink is a language highly applied by industry in the development of safety-critical embedded, real-time, and cyber-physical systems, where the establishment of accessible verification support can have substantial impact. This VeTSS project has made a crucial step forward in this area by provision of theorem proving technology in Isabelle/UTP, validated by its application to a real-world aircraft cabin-pressure control application from our company.”– Colin O’Halloran, CEO, D-RisQ –
