×

Statistical model checking of stochastic component-based systems. (English) Zbl 07192076

Summary: Behaviour-interaction-priority (BIP) is a component-based framework that supports the rigorous design of embedded systems. This paper discusses stochastic BIP (SBIP) component systems, which involve semantics-based Markov chain models. We develop a method to translate the systems from SBIP into the models specified in the PRISM language. A bisimulation minimization approach is proposed to overcome the problem of state-space explosion of model checking. Finally, to illustrate the effectiveness of the proposed methods, we discuss a case study involving clock synchronization protocols for statistical and probabilistic model checking.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
60J20 Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.)

Software:

PRISM; PRISM
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Basu A, Bozga M, Sifakis J. Modeling heterogeneous real-time components in BIP. In: Van Hung D, editor. Fourth IEEE international conference on software engineering and formal methods, 2006 (SEFM 2006). Washington, DC: IEEE; 2006. p. 3-12. [Google Scholar]
[2] Bensalem S, Bozga M, Delahaye B, et al. Statistical model checking QOS properties of systems with SBIP. In: Margaria T, Steffen B, editors. Leveraging applications of formal methods, verification and validation. Technologies for mastering change. Berlin: Springer; 2012. p. 327-341. [Google Scholar]
[3] Nouri A, Bensalem S, Bozga M, et al. Statistical model checking QOS properties of systems with SBIP. Int J Softw Tools Technol Transfer. 2014;17(2):171-185. doi: 10.1007/s10009-014-0313-6[Crossref], [Web of Science ®], [Google Scholar]
[4] Laplante S, Lassaigne R, Magniez F, et al. Probabilistic abstraction for model checking: an approach based on property testing. ACM Trans Comput Logic. 2007;8(4):20. doi: 10.1145/1276920.1276922[Crossref], [Web of Science ®], [Google Scholar] · Zbl 1367.68197
[5] Younes HL. Verification and planning for stochastic processes with asynchronous events. DTIC Document; 2005. [Google Scholar]
[6] Wald A. Sequential tests of statistical hypotheses. Ann Math Statist. 1945;16(2):117-186. doi: 10.1214/aoms/1177731118[Crossref], [Google Scholar] · Zbl 0060.30207
[7] Falcone Y, Jaber M, Nguyen TH, et al. Runtime verification of component-based systems. In: Barthe G, Pardo A, Schneider G, editors. Software engineering and formal methods. Berlin: Springer; 2011. p. 204-220. [Google Scholar] · Zbl 1350.68060
[8] Kwiatkowska M, Norman G, Parker D. PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan G, Qadeer S, editors. Proceedings of the 23rd International Conference on Computer Aided Verification (CAV’11); LNCS; Vol. 6806. Berlin: Springer; 2011. p. 585-591. [Google Scholar]
[9] Puterman ML. Markov decision processes. In: D.P. Heyman, M.J. Sobel, editors. Handbooks in operations research and management science; 1990. Vol. 2. p. 331-434. [Google Scholar] · Zbl 0703.90091
[10] Kwiatkowska M, Norman G, Parker D, et al. Performance analysis of probabilistic timed automata using digital clocks. Form Methods Syst Des. 2006;29(1):33-78. doi: 10.1007/s10703-006-0005-2[Crossref], [Web of Science ®], [Google Scholar] · Zbl 1105.68063
[11] Aziz A, Singhal V, Balarin F, et al. It usually works: the temporal logic of stochastic systems. In: Wolper P, editor. Computer aided verification. Berlin: Springer; 1995. p. 155-165. [Google Scholar]
[12] Bianco A, De Alfaro L. Model checking of probabilistic and nondeterministic systems. In: Thiagarajan PS, editor. Foundations of software technology and theoretical computer science. Berlin: Springer; 1995. p. 499-513. [Google Scholar] · Zbl 1354.68167
[13] Vardi MY. Probabilistic linear-time model checking: an overview of the automata-theoretic approach. Berlin Heidelberg: Springer; 1999. [Google Scholar]
[14] Sato T, Kameya Y. Prism: a language for symbolic-statistical modeling. Paper presented at IJCAI; NAGOYA, Aichi, Japan. Vol. 97; 1997. p. 1330-1339. [Google Scholar]
[15] Katoen JP, Kemna T, Zapreev I, et al. Bisimulation minimisation mostly speeds up probabilistic model checking. In: Grumberg O, Huth M, editors. International conference on tools and algorithms for the construction and analysis of systems. Berlin: Springer; 2007. p. 87-101. [Google Scholar] · Zbl 1186.68296
[16] Fisler K, Vardi MY. Bisimulation minimization and symbolic model checking. Form Methods Syst Des. 2002;21(1):39-78. doi: 10.1023/A:1016091902809[Crossref], [Web of Science ®], [Google Scholar] · Zbl 1018.68052
[17] Basu A, Bensalem S, Bozga M, et al. Statistical abstraction and model-checking of large heterogeneous systems. In: Hatcliff J, Zucca E, editors. Formal techniques for distributed systems. Berlin: Springer; 2010. p. 32-46. [Google Scholar]
[18] Bass RF. Stochastic processes. Vol. 33. Cambridge: Cambridge University Press; 2011. [Crossref], [Google Scholar] · Zbl 1247.60001
[19] Alur R, Henzinger T. Reactive modules. Form Methods Syst Des. 1999;15(1):7-48. doi: 10.1023/A:1008739929481[Crossref], [Web of Science ®], [Google Scholar]
[20] Ciesinski F, Größer M. On probabilistic computation tree logic. In: Baier C, Haverkort BR, Hermanns H, et al., editors Validation of stochastic systems. Berlin: Springer; 2004. p. 147-188. [Google Scholar] · Zbl 1203.68096
[21] Dehnert C, Katoen JP, Parker D. SMT-based bisimulation minimisation of Markov models. In: Giacobazzi R, Berdine J, Mastroeni I, editors. International workshop on verification, model checking, and abstract interpretation. Berlin: Springer; 2013. p. 28-47. [Google Scholar] · Zbl 1426.68168
[22] Jansen DN, Katoen JP, Oldenkamp M, et al. How fast and fat is your probabilistic model checker? An experimental performance comparison. In: Karen Y, editor. Haifa verification conference. Berlin: Springer; 2007. p. 69-85. [Google Scholar]
[23] Sen K, Viswanathan M, Agha G. Statistical model checking of black-box probabilistic systems. In: Alur, Rajeev, Peled, Doron, editors. Computer aided verification. Berlin: Springer; 2004. p. 202-215. [Google Scholar] · Zbl 1103.68639
[24] Legay A, Delahaye B, Bensalem S. Statistical model checking: an overview. In: Barringer H, Falcone Y, Finkbeiner B, et al., editors. Runtime verification. Berlin: Springer; 2010. p. 122-135. [Google Scholar]
[25] Sen K, Viswanathan M, Agha G. On statistical model checking of stochastic systems. In: Etessami K, Rajamani, Sriram K, editors. Computer aided verification. Berlin: Springer; 2005. p. 266-280. [Google Scholar] · Zbl 1081.68635
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.