Compositional Verification of Simulink Block Diagrams Using tock-CSP and CSP-Prover.

The analysis of timed process networks, such as Simulink multi-rate block diagrams, is challenging, particularly for large and complex diagrams whose verification might easily lead to the state explosion problem. For systems of this nature, with an acyclic communication graph, Roscoe and Dathi conceived a compositional deadlock verification strategy by means of local analyses, where only pairs of components need to have their behaviour analysed. Unfortunately, this strategy is restricted to untimed models. In this paper, we extend this strategy to tock-CSP, a dialect of CSP that allows modelling time aspects using a special tock event. This is implemented as a new package in CSP-Prover, a theorem prover for CSP which is itself implemented in Isabelle/HOL. An example demonstrates the benefits of our approach to deadlock analysis of Simulink block diagrams.