This paper describes an approach to the analysis of time-dependent 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, simulation and translation into UPPAAL/Timed Automata, for exhaustive state space verification, of modular TimePN models. The paper discusses the potential of the proposed approach through its application to a real-time system model.
Modular Modelling and Analysis of Time-dependent Systems
Cicirelli F;FURFARO, Angelo;PUPO, Francesco
2005-01-01
Abstract
This paper describes an approach to the analysis of time-dependent 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, simulation and translation into UPPAAL/Timed Automata, for exhaustive state space verification, of modular TimePN models. The paper discusses the potential of the proposed approach through its application to a real-time system model.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
