Journal Article

Correctness verification and performance analysis of real-time systems using stochastic preemptive time Petri nets

Vicario, E., Sassoli, L., Bucci, G.

2005

Overview

Time Petri nets describe the state of a timed system through a marking and a set of clocks. If clocks take values in a dense domain, state space analysis must rely on equivalence classes. These support verification of logical sequencing and quantitative timing of events, but they are hard to be enriched with a stochastic characterization of nondeterminism necessary for performance and dependability evaluation. Casting clocks into a discrete domain overcomes the limitation, but raises a number of problems deriving from the intertwined effects of concurrency and timing. We present a discrete-time variant of time Petri nets, called stochastic preemptive time Petri nets, which provides a unified solution for the above problems through the adoption of a maximal step semantics in which the logical location evolves through the concurrent firing of transition sets. We propose an analysis technique, which integrates the enumeration of a succession relation among sets of timed states with the calculus of their probability distribution. This enables a joint approach to the evaluation of performance and dependability indexes as well as to the verification of sequencing and timeliness correctness. Expressive and analysis capabilities of the model are demonstrated with reference to a real-time digital control system.

• Publisher: IEEE,IEEE Computer Society
• Subject: Casting / Clocks / Concurrent computing / confusion / correctness verification / discrete time / Index Terms- Real-time reactive systems / Mathematical models / maximal step semantics / Performance analysis / performance and dependability evaluation / Performance evaluation / Petri nets / Preempting / preemptive scheduling / Probability / Probability distribution / Program verification (computers) / Real time systems / Semantics / Sequencing / Software engineering / State-space methods / Stochastic models / stochastic preemptive Time Petri nets / Stochastic processes / Stochastic systems / Stochasticity / Studies / Timing / well definedness