Automatic Transformation of Ordinary Timed Petri Nets into Event-B for Formal Verification
The behavioral correctness of real-time software system relies on both the result of its computation and the clock times when the result is produced. Obviously, formal verification of the safety and correctness of real-time software specification from the very beginning of the software design phase obviously helps us reduce the development efforts. From a practical point of view, the timed Petri net is commonly used to graphically model and illustrate the views of the timed behaviors of the real-time software system. However, the simulation of a timed Petri net is tedious and ineffective for the huge and complex real-time system. Alternatively, formal verification using Event-B specification method provides an efficient automatic theorem proving tool but writing an Event-B specification from scratch is still difficult and needs mathematical logic background. In this paper, we propose an automatic transformation of ordinary timed Petri nets into Event-B specification. The basic notations in the ordinary timed Petri nets are considered and mapped into the code fragments of Event-B. The final resulting Event-B codes are generated in the well-formed format which is required and successfully verified by an Event-B prover called Rodin tool.
Authors who publish with Engineering Journal agree to transfer all copyright rights in and to the above work to the Engineering Journal (EJ)'s Editorial Board so that EJ's Editorial Board shall have the right to publish the work for nonprofit use in any media or form. In return, authors retain: (1) all proprietary rights other than copyright; (2) re-use of all or part of the above paper in their other work; (3) right to reproduce or authorize others to reproduce the above paper for authors' personal use or for company use if the source and EJ's copyright notice is indicated, and if the reproduction is not made for the purpose of sale.