Abstract
This invited paper surveys several simulation-based approa-ches to compute the probability of rare bugs in complex systems. The paper also describes how those techniques can be implemented in the professional toolset Plasma.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)
Baier, C., Katoen, J.-P.: Principles of Model Checking. Representation and Mind Series. The MIT Press, Cambridge (2008)
Boyer, B., Corre, K., Legay, A., Sedwards, S.: PLASMA-lab: a flexible, distributable statistical model checking library. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 160–164. Springer, Heidelberg (2013)
Cérou, F., Del Moral, P., Furon, T., Guyader, A.: Sequential Monte Carlo for rare event estimation. Stat. Comput. 22, 795–808 (2012)
Cérou, F., Guyader, A.: Adaptive multilevel splitting for rare event analysis. Stoch. Anal. Appl. 25, 417–443 (2007)
Clarke, E., Emerson, E.A., Sifakis, J.: Model checking: algorithmic verification and debugging. Commun. ACM 52(11), 74–84 (2009)
Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B., van Vliet, J., Wang, Z.: Statistical model checking for networks of priced timed automata. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 80–96. Springer, Heidelberg (2011)
Del Moral, P.: Feynman-Kac Formulae: Genealogical and Interacting Particle Systems with Applications. Probability and Its Applications. Springer, New York (2004)
Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453–457 (1975)
Itai, A., Rodeh, M.: Symmetry breaking in distributed networks. Inf. Comput. 88(1), 60–87 (1990)
Jegourel, C., Legay, A., Sedwards, S.: Cross-entropy optimisation of importance sampling parameters for statistical model checking. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 327–342. Springer, Heidelberg (2012)
Jegourel, C., Legay, A., Sedwards, S.: Importance splitting for statistical model checking rare properties. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 576–591. Springer, Heidelberg (2013)
Jegourel, C., Legay, A., Sedwards, S.: An Effective Heuristic for Adaptive Importance Splitting in Statistical Model Checking. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014, Part II. LNCS, vol. 8803, pp. 143–159. Springer, Heidelberg (2014)
Jegourel, C., Legay, A., Sedwards, S., Traonouez, L.-M.: Distributed verification of rare properties using importance splitting observers. In: ECEASST, vol. 72 (2015)
Kahn, H.: Stochastic (Monte Carlo) attenuation analysis. Technical report P-88, Rand Corporation, July 1949
Kahn, H.: Random sampling (Monte Carlo) techniques in neutron attenuation problems. Nucleonics 6(5), 27 (1950)
Kahn, H., Harris, T.E.: Estimation of particle transmission by random sampling. In: Applied Mathematics. Series 12, vol. 5. National Bureau of Standards (1951)
Kahn, H., Marshall, A.W.: Methods of reducing sample size in Monte Carlo computations. Oper. Res. 1(5), 263–278 (1953)
Lehmann, D., Rabin, M.O.: On the advantage of free choice: a symmetric and fully distributed solution to the dining philosophers problem. In: Proceedings of the 8th Annual Symposium on Principles of Programming Languages, pp. 133–138 (1981)
Maler, O., Larsen, K.G., Krogh, B.H.: On zone-based analysis of duration probabilistic automata. In: 12th International Workshop on Verification of Infinite-State Systems (INFINITY), pp. 33–46 (2010)
Okamoto, M.: Some inequalities relating to the partial sum of binomial probabilities. Ann. Inst. Stat. Math. 10, 29–35 (1959)
Ridder, A.: Importance sampling simulations of markovian reliability systems using cross-entropy. Ann. Oper. Res. 134, 119–136 (2005)
Rosenbluth, M.N., Rosenbluth, A.W.: Monte Carlo calculation of the average extension of molecular chains. J. Chem. Phys. 23(2) (1955)
Rubinstein, R.: The cross-entropy method for combinatorial and continuous optimization. In: Methodology and Computing in Applied Probability, vol. 1, pp. 127–190. Kluwer Academic (1999)
Wald, A.: Sequential tests of statistical hypotheses. Ann. Math. Stat. 16(2), 117–186 (1945)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Legay, A., Sedwards, S., Traonouez, LM. (2016). Rare Events for Statistical Model Checking an Overview. In: Larsen, K., Potapov, I., Srba, J. (eds) Reachability Problems. RP 2016. Lecture Notes in Computer Science(), vol 9899. Springer, Cham. https://doi.org/10.1007/978-3-319-45994-3_2
Download citation
DOI: https://doi.org/10.1007/978-3-319-45994-3_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-45993-6
Online ISBN: 978-3-319-45994-3
eBook Packages: Computer ScienceComputer Science (R0)