Timed state space analysis of real-time preemptive systems

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.