From Place/Transition Petri nets to B abstract machines for safety critical systems

Fulfilling the safety requirements is one of the most serious and problematic issues in critical systems design and safety critical software development. In this context, thanks to their analysis power, formal methods have been widely used in the various stages of the design and the implementation of safety critical systems. However, some methods such as the B method, although well adapted to safety issues, are still poorly used in large scale industrial environment. The purpose of this paper is to present a methodology of Place/Transition Petri nets transformation into B abstract machines enabling an interesting combination of the graphical modeling power of Petri nets and the verification tools of the B method. In fact, translating a Petri net to a B abstract machine can have many advantages such as the generation of code, the integration of safety invariants or the aggregation with other formal models. Therefore, the B verification will enlarge the scope of its applicability by having a new modeling alternative and passing through model transformation. An illustrative example of the transformation is presented for a railway study case.