Combining Model Checking and Discrete-Event Supervisor Synthesis

We present an approach to facilitate the design of provably correct concurrent sys-tems by recasting recent work that uses discrete-event supervisor synthesis to auto-matically 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 infor-mal specification Ein, the preparation step is assumed to yield a formal specifica-tion E of the allowed system behaviours and two versions of C: Ce to identify the specification-relevant events in C and enable supervisor synthesis, and Ce,a to intro-duce “checkable redundancy ” and used during the analysis step to locate bugs in: the specification formalization E, the event markup in Ce, or the implementation of the synthesis. The result is supervised Promela code Csup that is more likely to be correct with respect to E and Ein. The approach is illustrated with an example. A prototype tool implementing the approach is described