Verification of Real-Time Embedded Systems using Petri Net Models and Timed Automata
2002 (English)In: 8th International Conference on Real-Time Computing Systems and Applications RTCSA 2002,2002, 2002, 191-199 p.Conference paper (Refereed)
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.
Place, publisher, year, edition, pages
2002. 191-199 p.
real-time embedded systems, petri net, formal verification, timed automata
IdentifiersURN: urn:nbn:se:liu:diva-23365Local ID: 2801OAI: oai:DiVA.org:liu-23365DiVA: diva2:243679