Hier finden Sie wissenschaftliche Publikationen aus den Fraunhofer-Instituten.

A review of statistical model checking pitfalls on real-time stochastic models

: Bohlender, Dimitri


Margaria-Steffen, T. (Ed.):
Leveraging applications of formal methods, verification and validation. Specialized techniques and applications. 6th international symposium, ISoLA 2014. Vol.2 : Imperial, Corfu, Greece, October 8-11, 2014; Proceedings
Berlin: Springer, 2014 (Lecture Notes in Computer Science 8803)
ISBN: 978-3-662-45230-1 (Print)
ISBN: 978-3-662-45231-8 (Online)
ISBN: 3-662-45230-8
International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA) <6, 2014, Corfu>
International School on Tool-Based Rigorous Engineering of Software Systems (STRESS) <3, 2014, Corfu>
Fraunhofer IESE ()
Statistical Model Checking (SMC)

Statistical model checking (SMC) is a technique inspired by Monte-Carlo simulation for verifying time-bounded temporal logical properties. SMC originally focused on fully stochastic models such as Markov chains, but its scope has recently been extended to cover formalisms that mix functional real-time aspects, concurrency and non-determinism. We show by various examples using the tools UPPAAL SMC and Modes that combining the stochastic interpretation of such models with SMC algorithms is extremely subtle. This may yield significant discrepancies in the analysis results. As these subtleties are not so obvious to the end-user, we present five semantic caveats and give a classification scheme for SMC algorithms. We argue that caution is needed and believe that the caveats and classification scheme in this paper serve as a guiding reference for thoroughly understanding them.