Abstract
Bounded timed-arc Petri nets with read-arcs were recently proven equivalent to networks of timed automata, though the Petri net model cannot express urgent behaviour and the described mutual trans- lations are rather inefficient. We propose an extension of timed-arc Petri nets with invariants to enforce urgency and with transport arcs to generalise the read-arcs. We also describe a novel translation from the extended timed-arc Petri net model to networks of timed automata. The translation is implemented in the tool TAPAAL and it uses UPPAAL as the verification engine. Our experiments confirm the efficiency of the translation and in some cases the translated models verify significantly faster than the native UPPAAL models do.
Originalsprog | Engelsk |
---|---|
Bogserie | Lecture Notes in Computer Science |
Vol/bind | 5885 |
Sider (fra-til) | 698-716 |
Antal sider | 18 |
ISSN | 0302-9743 |
DOI | |
Status | Udgivet - 2009 |
Begivenhed | 11th International Conference on Formal Engineering Methods (ICFEM'09) - Rio de Janeiro, Brasilien Varighed: 8 dec. 2009 → 11 dec. 2009 Konferencens nummer: 11 |
Konference
Konference | 11th International Conference on Formal Engineering Methods (ICFEM'09) |
---|---|
Nummer | 11 |
Land/Område | Brasilien |
By | Rio de Janeiro |
Periode | 08/12/2009 → 11/12/2009 |
Bibliografisk note
Titel:11th International Conference on Formal Engineering Methods (ICFEM'09)
Oversat titel:
Oversat undertitel:
Forlag:
Springer
ISBN (Trykt):
978-3-642-10372-8
ISBN (Elektronisk):
Publikationsserier:
Lecture Notes in Computer Science, Lecture Notes in Comptuer Science, 0302-9743, 1611-3349, 5885
Emneord
- timed-arc Petri nets
- verification