Model Checking Time Petri Nets: A Translation Approach based on Uppaal and a Case Study
| Title | Model Checking Time Petri Nets: A Translation Approach based on Uppaal and a Case Study |
| Publication Type | Conference Paper |
| Year of Publication | 2005 |
| Authors | Furfaro, A, Nigro, L |
| Conference Name | Proc. IASTED International Conference on Software Engineering (SE'05) |
| Date Published | February 15-17 |
| Conference Location | Innsbruck, Austria |
| Abstract | This work is concerned with modelling and analysis of time dependent systems, e.g. communication protocols and embedded real-time systems, using Merlin and Farber's Time Petri Nets (TPN's). TPN's combine a rigorous formalism for expressing time requirements with a familiar graphical notation. The practical use of TPN's, though, strongly depends on adequate tools supporting the verification activities. This paper proposes a translation approach of TPN's on to UPPAAL/Timed Automata which makes it possible to model check realistic TPN systems using a popular tool. The method centres on a single and general UPPAAL template which can easily be decorated for verification purposes. The paper demonstrates effectiveness of the approach through a case study. |