The EventB2PN Tool: From Event-B Specification to Petri Nets through Model Transformation
| Affiliation auteurs | !!!! Error affiliation !!!! |
| Titre | The EventB2PN Tool: From Event-B Specification to Petri Nets through Model Transformation |
| Type de publication | Conference Paper |
| Year of Publication | 2015 |
| Auteurs | Garoui M, Mazigh B, Koukam A |
| Editor | Saisho K |
| Conference Name | 2015 16TH IEEE/ACIS INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, ARTIFICIAL INTELLIGENCE, NETWORKING AND PARALLEL/DISTRIBUTED COMPUTING (SNPD) |
| Publisher | IEEE; ACIS |
| Conference Location | 345 E 47TH ST, NEW YORK, NY 10017 USA |
| ISBN Number | 978-1-4799-8676-7 |
| Résumé | 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. |