loading...
A Translation Based Method for the Timed Analysis of Scheduling Extended Time Petri Nets
Lisbon, Portugal December 05-December 08
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/REAL.2004.925th IEEE International Real-Time Sys ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Didier Lime, Institut de Recherche en Communication et Cybernétique de Nantes
Olivier (H.) Roux, Institut de Recherche en Communication et Cybernétique de Nantes
In this paper, we present a method for the timed analysis of real-time systems, taking into account the scheduling constraints. The model considered is an extension of time Petri nets, Scheduling Extended Time Petri Nets (SETPN) for which the valuations of transitions may be stopped and resumed, thus allowing the modelling of preemption. This model has a great expressivity and allows a very natural modelling. The method we propose consists of precomputing, with a fast algorithm, the state space of the SETPN as a stopwatch automaton (SWA). This stopwatch automaton is proven timed bisimilar to the SETPN, so we can perform the timed analysis of the SETPN through it with the tool on linear hybrid automata, HYTECH. The main interests of this pre-computation are that it is fast because it is Difference Bounds Matrix (DBM)-based, and that it has online stopwatch reduction mechanisms. Consequently, the resulting stopwatch automaton has, in the general case, a fairly lower number of stopwatches than what could be obtained by a direct modelling of the system as SWA. Since the number of stopwatches is critical for the complexity of the verification, the method increases the efficiency of the timed analysis of the system, and in some cases may just make it possible at all.
Citation:
Didier Lime, Olivier (H.) Roux, "A Translation Based Method for the Timed Analysis of Scheduling Extended Time Petri Nets," rtss, pp.187-196, 25th IEEE International Real-Time Systems Symposium (RTSS'04), 2004
Usage of this product signifies your acceptance of the Terms of Use.