CSL Model Checking of Deterministic and Stochastic Petri Nets

Konferenz: MMB 2006 - 13th GI/ITG Conference Measuring, Modelling and Evaluation of Computer and Communication Systems
27.03.2006 - 29.03.2006 in Nürnberg, Germany

Tagungsband: MMB 2006

Seiten: 18Sprache: EnglischTyp: PDF

Persönliche VDE-Mitglieder erhalten auf diesen Artikel 10% Rabatt

Martínez, José M.; Haverkort, Boudewijn R. (Faculty of Electrical Engineering, Mathematics and Computer Science, University of Twente, The Netherlands)

Deterministic and Stochastic Petri Nets (DSPNs) are widely used for modeling discrete-event systems where events may occur either without consuming time, after a deterministic time, or after an exponentially distributed time. The underlying process defined by DSPNs, under certain restrictions, corresponds to a class of Markov Regenerative Processes (MRGP). In this paper, we investigate the use of CSL (Continuous Stochastic Logic) to express probabilistic properties, such as time-bounded until and time-bounded next, at the DSPN level. The verification of such properties requires the solution of the steady-state and transient probabilities of the underlying MRGP. We also address a number of semantic issues regarding the application of CSL for MRGP and provide numerical model checking algorithms for this logic. A prototype model checker, based on SPNica, is also described.