Mechanised local deadlock analysis based on timed behavioural patterns and responsiveness

Abstract

Although semi-formal model driven development (MDD) helps the identification of design problems in the early stages of the development using simulation environments such as Matlab/SIMULINK, the most recent guidelines for verification in this context (such as DO178C) suggest the use of formal verification for such systems. In this context, many approaches have been proposed to perform translations from SIMULINK to a target formal notation. However, most of these approaches are not focused on compositional verification to allow scalability; or do not provide traceability of the formal verification results. To provide a compositional deadlock analysis for timed process networks, more specifically, those obtained from SIMULINK discrete multi-rate block diagrams, we present a strategy that uses Communicating Sequential Processes (CSP) to verify these models. The strategy extends the Roscoe and Dathi’s compositional deadlock analysis theory by adding time. Moreover, the approach handles both: models with an acyclic communication graph; and cyclic models, which naturally happens in SIMULINK models with feedback, among other kinds of cycles. Since there is no general solution to analyse cyclic models in a compositional way, we explore the use of behavioural patterns that allow the verification to be carried out in a compositional fashion. Besides, we devise a verification approach for the integration of systems by extending the notion of responsive plug-ins from Roscoe, Reed and Sinclair. We represent process networks in tock-CSP, a dialect of CSP that allows modelling time aspects using a special tock event. The verification approach is encoded in CSP-Prover, a theorem prover for CSP which is itself implemented in Isabelle/HOL. To illustrate the overall approach and, particularly, how it can scale, we consider an example of an actuation system with increasing complexity for the longitudinal control of an aircraft, including an Elevator Control System and an example of an active Stall Control System. We show that the examples are instances of the considered timed behaviour patterns. These patterns and all verification steps are formalised using CSP-Prover. Soundness is based on a Galois connection linking the traces semantics of the generated tock-CSP specification and simulation trajectories resulting from an encoding in Isabelle/HOL of the Bouissou and Chapoutot’s operational semantics theory for SIMULINK.