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

Authors

  • Chalika Saksupawattanakul Chulalongkorn University
  • Wiwat Vatanawood Chulalongkorn University

DOI:

https://doi.org/10.4186/ej.2018.22.4.161

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.

Downloads

Download data is not yet available.

Author Biographies

Chalika Saksupawattanakul

Department of Computer Engineering, Faculty of Engineering, Chulalongkorn University,

Bangkok 10330, Thailand

Wiwat Vatanawood

Department of Computer Engineering, Faculty of Engineering, Chulalongkorn University,

Bangkok 10330, Thailand

Downloads

Published In
Vol 22 No 4, Jul 31, 2018
How to Cite
[1]
C. Saksupawattanakul and W. Vatanawood, “Automatic Transformation of Ordinary Timed Petri Nets into Event-B for Formal Verification”, Eng. J., vol. 22, no. 4, pp. 161-175, Jul. 2018.