Model checking time-dependent system specifications using Time Stream Petri Nets and Uppaal

This paper describes an approach to modeling and analysis of time-dependent system specifications which is based on the Time Stream Petri Nets (TSPNs) formalism. The work argues that although TSPNs were originally proposed for modeling 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 model checking in terms of Uppaal timed automata, which permit behavioural analysis and in particular schedulability analysis of task executions in real-time specifications. Property analysis rests on the construction of a (hopefully finite) zone state graph of a TSPN model and its efficient traversal by Uppaal verifier, which in turn represents an effective approach for dealing with infinite computations in a compact way. The paper introduces the TSPN formalism and focuses on the implemented structural translation onto Uppaal which is assisted by a library of reusable template processes. The modeling/analysis techniques are demonstrated by two examples. The first example deals with project management, i.e. the exhaustive analysis of general CPM/PERT project models where an activity duration is expressed by a time interval. The second example is related to a thoroughly analysis of the temporal behaviour of a complex embedded real-time system with timing constraints. An indication of on-going and future work is, finally, given in the conclusions. Soundness of the structural translation is shown by a formal proof reported in appendix.