The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.02 - February (2004 vol.30)
pp: 97-111
ABSTRACT
<p><b>Abstract</b>—A modeling notation is introduced which extends Time Petri Nets with an additional mechanism of resource assignment making the progress of timed transitions be dependent on the availability of a set of preemptable resources. The resulting notation, which we call Preemptive Time Petri Nets, permits natural description of complex real-time systems running under preemptive scheduling, with periodic, sporadic, and one-shot processes, with nondeterministic execution times, with semaphore synchronizations and precedence relations deriving from internal task sequentialization and from interprocess communication, running on multiple processors. A state space analysis technique is presented which supports the validation of Preemptive Time Petri Net models, combining tight schedulability analysis with exhaustive verification of the correctness of logical sequencing. The analysis technique partitions the state space in equivalence classes in which timing constraints are represented in the form of Difference Bounds Matrixes. This permits it to maintain a polynomial complexity in the representation and derivation of state classes, but it does not tightly encompass the constraints deriving from preemptive behavior, thus producing an enlarged representation of the state space. False behaviors deriving from the approximation can be cleaned-up through an algorithm which provides a necessary and sufficient condition for the feasibility of a behavior along with a tight estimation of its timing profile.</p>
INDEX TERMS
Hard real-time systems, reactive systems, preemptive scheduling, interprocess communication, nondeterministic time parameters, multiprocessor schedulability, timeliness predictability, state space analysis, Preemptive Time Petri Nets.
CITATION
Giacomo Bucci, Andrea Fedeli, Luigi Sassoli, Enrico Vicario, "Timed State Space Analysis of Real-Time Preemptive Systems", IEEE Transactions on Software Engineering, vol.30, no. 2, pp. 97-111, February 2004, doi:10.1109/TSE.2004.1265815
21 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool