Modelling and Analysing Real Time System Specifications using Time Stream Petri Nets

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.