The EventB2PN Tool: From Event-B specification to Petri Nets through model transformation

Formal methods, in particular the B Method and its extension Event-B are used to validate the system correctness and to verify its properties. The weak point here is that Event-B that don´t support quantitative analysis of performance and/or dependability. For this reason, we transform an Event-B specification to another formalism which automatically transform and allows us to evaluate the performance and/or dependability attributes. In this paper, we propose an algorithm which offers the transformation rules. This algorithm is implemented within our transformation tool, EventB2PN, to generate the transformation process from Event-B specification to Petri Net (PN) structure. EventB2PN tool use XML file for Event-B specification and standard PNML file for PN which can be analyzed with quantitative analysis tool. A small case study of repaired system has been conducted to show the benefits and the strong points in ours works.