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 |
| Volume | 8 |
| Pagination | 8–20 |
| Abstract | 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. |