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.
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.
[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. |
|
