A. Furfaro and L. Nigro (Italy)
Time Petri nets, model checking, translation approach, timed automata, UPPAAL.
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.
Important Links:
Go Back
