This paper describes an approach to modelling and analysis of real-time system specifications which is based on the Time Stream Petri Nets (TSPNs) formalism. The work argues that although TSPNs were originally proposed for modelling multimedia/hypermedia systems, they are well suited for expressing timing constraints in general time-dependent systems. The approach is assisted by some developed tools, based on discrete-event simulation and on model checking in terms of Uppaal timed automata, which permit property analysis of timing constraints and in particular schedulability analysis of task executions in real-time specifications. The paper introduces the TSPN formalism and describes an implemented transformation in Uppaal. The modelling/analysis approach is demonstrated by an example. Finally, an indication of further work is given in the conclusions.
Modelling and Analysing Real Time System Specifications using Time Stream Petri Nets
FURFARO, Angelo;NIGRO, Libero
2009-01-01
Abstract
This paper describes an approach to modelling and analysis of real-time system specifications which is based on the Time Stream Petri Nets (TSPNs) formalism. The work argues that although TSPNs were originally proposed for modelling multimedia/hypermedia systems, they are well suited for expressing timing constraints in general time-dependent systems. The approach is assisted by some developed tools, based on discrete-event simulation and on model checking in terms of Uppaal timed automata, which permit property analysis of timing constraints and in particular schedulability analysis of task executions in real-time specifications. The paper introduces the TSPN formalism and describes an implemented transformation in Uppaal. The modelling/analysis approach is demonstrated by an example. Finally, an indication of further work is given in the conclusions.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.