Linköping University: Students Alumni Trade and Industry/Society Internal Search
RTCSA02

Verification of Real-Time Embedded Systems using Petri Net Models and Timed Automata

Luis Alejandro Cortes
 
Petru Eles Author homepage
Zebo Peng Author homepage

8th International Conference on Real-Time Computing Systems and Applications (RTCSA 2002), Tokyo, Japan, March 18-20, 2002, pp. 191-199.

ABSTRACT
There is a lack of new verification methods that overcome the limitations of traditional validation techniques and are, at the same time, suitable for real-time embedded systems. This paper presents an approach to formal verification of real-time embedded systems modeled in a timed Petri net representation. We translate the Petri net model into timed automata and use model checking to prove whether certain properties hold with respect to the system model. We propose two strategies to improve the efficiency of verification. First, we apply correctness-preserving transformations to the system model in order to obtain a simpler, yet semantically equivalent, one. Second, we exploit the structure of the system model by extracting its the sequential behavior. Experimental results demonstrate significant improvements in the efficiency of verification.


Related files:
RTCSA02.pdfAdobe Acrobat portable document
RTCSA02.ps.gzpostscript document, compressed (with gzip)


[AEP02] Luis Alejandro Cortes, Petru Eles, Zebo Peng, "Verification of Real-Time Embedded Systems using Petri Net Models and Timed Automata", 8th International Conference on Real-Time Computing Systems and Applications (RTCSA 2002), Tokyo, Japan, March 18-20, 2002, pp. 191-199.
( ! ) perl script by Giovanni Squillero with modifications from Gert Jervan   (v3.1, p5.2, September-2002-)