In: Ragunathan Rajkumar (Ed.): 25th IEEE International Real-Time Systems Symposium (RTSS'04), December 05 - 08, 2004, Lisbon, Portugal, pages 187-196. IEEE Press, December 2004.
Abstract: 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.