Combining Model Checking and Discrete-Event Supervisor Synthesis

Abstract

We present an approach to facilitate the design of provably correct concurrent systems by recasting recent work that uses discrete-event supervisor synthesis to automatically generate concurrency control code in Promela and combine it with model checking in Spin. This approach consists of the possibly repeated execution of three steps: manual preparation, automatic synthesis, and semi-automatic analysis. Given a concurrent Promela program C devoid of any concurrency control and an informal specification E_in , the preparation step is assumed to yield a formal specification E of the allowed system behaviours and two versions of C: C_e to identify the specification-relevant events in C and enable supervisor synthesis, and C_e,a to introduce “checkable redundancy” and used during the analysis step to locate bugs in: the specification formalization E, the event markup in C_e, or the implementation of the synthesis. The result is supervised Promela code C_sup that is more likely to be correct with respect to E and E_in. The approach is illustrated with an example. A prototype tool implementing the approach is described.