Automatic Transformation of Ordinary Timed Petri Nets into Event-B for Formal Verification

Abstract

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.