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

  • Chalika Saksupawattanakul Chulalongkorn University
  • Wiwat Vatanawood Chulalongkorn University

Downloads

Download data is not yet available.

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.

View article in other formats
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

Published
Vol 22 No 4, Jul 31, 2018
How to Cite
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.

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.

Article Statistics
Total PDF downloads: 34