Mechanised Assume-Guarantee Reasoning for Control Law Diagrams via Circus

Our project will explore the development of formal AG-based proof support for discrete-time Simulink diagrams through a semantic embedding of the Circus language in Isabelle/HOL. Circus is a formal modelling language for concurrent reactive systems in the style of CSP, but with support for modelling mutable state variables.

Simulink is a widely used industrial language and tool-set for expressing control law diagrams, including support for simulation and code generation. Though empirical analysis through simulation is an important technique to explore and refine models, only formal verification can make specific mathematical guarantees about behaviour, which is crucial to ensure safety of associated implementations.

Whilst verification facilities for Simulink exist there is still a need for assertional reasoning techniques that capture the full range of specifiable behaviour, provide non-deterministic specification constructs, and support compositional verification. Applicable tool support for these techniques with a high degree of automation is also of vital importance to enable adoption by industry. Since Simulink diagrams are data rich and usually have an uncountably infinite state space, model checking alone is insufficient and there is a need for theorem proving facilities.

Assume-Guarantee (AG) reasoning is a valuable compositional verification technique for reactive systems In AG, one demonstrates composite system level properties by decomposing them into a number of contracts for each component subsystem. Each contract specifies the guarantees that the subsystem will make about its behaviour, under certain specified assumptions of the subsystem’s environment. Such a decomposition is vital in order to make verification of a complex system tractable, and to allow development of subsystems by separate teams.

AG reasoning has previously been applied to verification of discrete time Simulink control law diagrams through mappings into synchronous languages like Lustre and Kahn Process Networks. However such formalisms, whilst theoretically and practically appealing, are limited to expressing processes that are inherently deterministic and non-terminating in nature. Thus, it is necessary to translate to several additional notations where AG verification can be performed, which hampers both traceability and composition with other languages of different paradigms. What is needed is a rich unified language capable of AG reasoning, and supported by theorem proving, into which Simulink and associated notations can be losslessly translated.

The project has the potential to greatly benefit industrial users of Simulink by providing further analysis facilities which can be applied when constructing assurance cases and our results in AG reasoning facilities will be transferrable to reasoning about models in other domains, such as programming languages. Moreover our contract notion is theoretically not limited to only discrete traces, but also to piecewise continuous functions. Therefore the work on this project could feed into future support for continuous and hybrid Simulink diagrams as well. Moreover, the work, being based in the UTP, is not limited to just Simulink but can also, for example, be applied to programming languages and also Modelica models, potentially supported by our associated hybrid semantics.

Researchers: Jim Woodcock and Simon Foster, University of York