Combining Model Checking and Discrete-Event Supervisor Synthesis

Nicolas Chausse, Helen Xu, Juergen Dingel, Karen Rudie


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.

Full Text:




Hosted By Universitätsbibliothek TU Berlin.