UsingTPN/Designer and Uppaal for Modular Modelling and Analysis of Time-critical Systems
|Title||UsingTPN/Designer and Uppaal for Modular Modelling and Analysis of Time-critical Systems|
|Publication Type||Journal Article|
|Year of Publication||2007|
|Authors||Cicirelli, F, Furfaro, A, Nigro, L|
|Journal||International Journal of Simulation Systems, Science & Technology|
This paper describes an approach to the analysis of time-critical systems which combines discrete- event simulation and model-checking techniques. The approach rests on Merlin and Farber’s Time Petri Nets (TimePNs) and is supported by a Java toolbox −TPN/DESIGNER− which enables graphical modelling and simulation of modular TimePN models. The toolbox also allows translation of a TimePN model into UPPAAL/Timed Automata for exhaustive state space verification. Usefulness and potential of the proposed approach are demonstrated through its application to a real-time system example.