Abstract:
In the engineering of non-functional requirements, verification of quantitative properties of stochastic models enables early assessment of design choices and provides a model driven guidance for implementation and integration stages, with notable impact in the development of systems exposed to the intertwined effects of concurrency and stochastic durations.
To this end, probabilistic model checking supports a systematic practice through which the same model can be verified against multiple probabilistic properties specified in some well defined language, able to analyze the impact on quality of different patterns of behavior, and open to automated regression verification when the model evolves.
A number of techniques and tools have been proposed, based on statistical discrete event simulation or on numerical solution, the latter aiming at accuracy and confidence at the expense of restrictions on the class of models amenable to verification. In particular, if all model durations are exponentially distributed (EXP), the underlying stochastic process of the model falls in the class of Continuous Time Markov Chains (CTMC), the model always satisfies the Markov condition, and an efficient numerical solution can be attained by composition of behaviors [BHHK03,CHKM09,DHS09].
However, model validity often requires that some durations break the EXP memoryless property and be rather generally distributed (GEN). For instance, this occurs in aging processes accumulating memory over time, or in real-time systems or network protocols where correctness depends on firm time bounds. In these cases, the future evolution depends on the remaining time of GEN durations, and the underlying stochastic process may satisfy the Markov condition only at some regeneration points [BT95,CGL94,CKT94].
In this course:
we recall the basics of modeling systems using stochastic Petri Nets and illustrate their construction through the Oris tool [Oris], and we characterize different classes of stochastic processes that may underly a model depending on its structure, with emphasis on Continuous Time Markov Chains (CTMC), Semi Markov Processes (SMP), and Markov Regenerative Processes (MRP) [BT95,CGL94,CKT94];
we illustrate through examples the motivations for numerical solution of models with concurrent stochastic non-Markovian durations, focusing on cases with multiple concurrent GEN durations with an underlying stochastic Markov Regenerative Process (MRP);
we describe the salient traits of numerical solution of reachability analysis for this class of models through the method of stochastic state classes [CGV09,VSC09,HPRV12];
we describe a novel technique that extends the method to solve a problem of probabilistic model checking emphasizing challenges, achieved results, and structural limits that arise when non-Markovian regenerative analysis is cast in the shape of probabilistic model checking [HPRV11,PHV15].
[BHHK03] C.Baier, B.Haverkort, H.Hermanns, J.P.Katoen,"Model-checking algorithms for continuous-time Markov chains," Transactions on Software Engineering, 2003.
[BT95] A.Bobbio, M.Telek, "Markov regenerative SPN with non-overlapping activity cycles," IPDS95.
[CGL94] GF.Ciardo, R.German, C.Lindemann, "A characterization of the stochastic process underlying a stochastic Petri net," IEEE Transactions on Software Engineering, 1994.
[CGV09] L.Carnevali, L.Grassi, E.Vicario, "State-density functions over DBM domains in the analysis of non-Markovian models", IEEE Trans. on Software Engineering, 2009.
[CHKM09] T.Chen, T.Han, J.P.Katoen, A.Mereacre, "Quantitative model checking of continuous-time Markov chains against timed automata specifications," LICS’09.
[CKT94] H.Choi, V.G.Kulkarni, K.S.Trivedi, "Markov Regenerative stochastic Petri Nets," Performance Evaluation 1994.
[DHS09] S.Donatelli, S.Haddad, J.Sproston, "Model checking Timed and Stochastic Properties with CSL-TA," Transactions on Software Engineering, 2009.
[HPRV11] A.Horváth, M.Paolieri, L.Ridi, E.Vicario, "Probabilistic Model Checking of non-Markovian Models with Concurrent Generally Distributed Timers," QEST’11.
[HPRV12] A.Horváth, M.Paolieri, L.Ridi, E.Vicario, "Transient analysis of non-Markovian models using stochastic state classes," Performance Evaluation, 2012.
[PHV15] M.Paolieri, A.Horváth, E.Vicario "Probabilistic Model Checking of Regenerative Concurrent Systems," IEEE Trans. on Software Engineering, accepted and published on line August 2015.
[Oris] http://www.oris-tool.org/
[VSC09] E. Vicario, L. Sassoli, L. Carnevali, "Using Stochastic State Classes in Quantitative Evaluation of Dense-Time Reactive Systems", IEEE Trans. on Software Engineering, 2009.
