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.

Model Checking Time-Dependent System Specifications using Time Stream Petri Nets and Uppaal

FURFARO, Angelo;NIGRO, Libero
2012-01-01

Abstract

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.
2012
Modeling ,Timing constraints, Real-time constraints, Schedulability analysis, Time Stream Petri Nets, Model checking, Timed automata, Uppaal
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.11770/141607
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 16
  • ???jsp.display-item.citation.isi??? 16
social impact