2015/11/03 by Nicolas Chausse, Helen Xu, Chausse, Nicolas +5
Computer Science · #Formal Methods in Verification #Petri Nets in System Modeling #Distributed systems and fault tolerance
paper · doi:10.14279/tuj.eceasst.46.686
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 Ein , the preparation step is assumed to yield a formal specification 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 introduce “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.