research-article

Public Access

A Survey of Statistical Model Checking

Authors:

Karl PalmskogAuthors Info & Claims

ACM Transactions on Modeling and Computer Simulation (TOMACS), Volume 28, Issue 1

Article No.: 6, Pages 1 - 39

https://doi.org/10.1145/3158668

Published: 31 January 2018 Publication History

Abstract

Interactive, distributed, and embedded systems often behave stochastically, for example, when inputs, message delays, or failures conform to a probability distribution. However, reasoning analytically about the behavior of complex stochastic systems is generally infeasible. While simulations of systems are commonly used in engineering practice, they have not traditionally been used to reason about formal specifications. Statistical model checking (SMC) addresses this weakness by using a simulation-based approach to reason about precise properties specified in a stochastic temporal logic. A specification for a communication system may state that within some time bound, the probability that the number of messages in a queue will be greater than 5 must be less than 0.01. Using SMC, executions of a stochastic system are first sampled, after which statistical techniques are applied to determine whether such a property holds. While the output of sample-based methods are not always correct, statistical inference can quantify the confidence in the result produced. In effect, SMC provides a more widely applicable and scalable alternative to analysis of properties of stochastic systems using numerical and symbolic methods. SMC techniques have been successfully applied to analyze systems with large state spaces in areas such as computer networking, security, and systems biology. In this article, we survey SMC algorithms, techniques, and tools, while emphasizing current limitations and tradeoffs between precision and scalability.

References

[1]

Alessandro Abate, Joost-Pieter Katoen, John Lygeros, and Maria Prandini. 2010. Approximate model checking of stochastic hybrid systems. Eur. J. Control 16, 6 (2010), 624--641.

[2]

C. J. Adcock. 1997. Sample size determination: A review. J. Roy. Stat. Soci. Ser. D (The Statistician) 46, 2 (1997), 261--283.

[3]

Gul Agha. 2013. Euclidean model checking: A scalable method for verifying quantitative properties in probabilistic systems. In Proceedings of the 5th International Conference on Algebraic Informatics (CAI’13), Traian Muntean, Dimitrios Poulakis, and Robert Rolland (Eds.). Springer, Berlin, Germany, 1--3.

[4]

Gul Agha, Carl Gunter, Michael Greenwald, Sanjeev Khanna, José Meseguer, Koushik Sen, and Prasanna Thati. 2005. Formal modeling and analysis of DoS using probabilistic rewrite theories. In Proceedings of the International Workshop on Foundations of Computer Security (PCS’05).

[5]

Gul Agha, José Meseguer, and Koushik Sen. 2006. PMaude: Rewrite-based specification language for probabilistic object systems. Electron. Notes Theoret. Comput. Sci. 153, 2 (2006), 213--239. Proceedings of the Third Workshop on Quantitative Aspects of Programming Languages (QAPL’05)

Digital Library

[6]

Musab AlTurki and José Meseguer. 2011. PVeStA: A parallel statistical model checking and quantitative analysis tool. In Proceedings of the 4th International Conference on Algebra and Coalgebra in Computer Science (CALCO’11), Andrea Corradini, Bartek Klin, and Corina Cîrstea (Eds.). Springer, Berlin, Germany, 386--392.

Digital Library

[7]

APMC. 2005. APMC2 tool. Retrieved from http://berbiqui.org/apmc2/apmc-2.0.0.tar.gz.

[8]

APMCBeta. 2014. APMC3 Beta tool. Retrieved from https://web.archive.org/web/20140928144328http://sylvain.berbiqui.org/apmc.

[9]

Alexandre Arnold, Massimo Baleani, Alberto Ferrari, Marco Marazza, Valerio Senni, Axel Legay, Jean Quilbeuf, and Christoph Etzien. 2016. An application of SMC to continuous validation of heterogeneous systems. In Proceedings of the 9th EAI International Conference on Simulation Tools and Techniques (SIMUTOOLS’16). 76--85.

Digital Library

[10]

Adnan Aziz, Kumud Sanwal, Vigyan Singhal, and Robert Brayton. 1996. Verifying continuous time Markov chains. In Proceedings of the 8th International Conference on Computer Aided Verification (CAV’96), Rajeev Alur and Thomas A. Henzinger (Eds.). Springer, Berlin, Germany, 269--276.

Digital Library

[11]

Adnan Aziz, Kumud Sanwal, Vigyan Singhal, and Robert Brayton. 2000. Model-checking continuous-time Markov chains. ACM Trans. Comput. Logic 1, 1 (July 2000), 162--170.

Digital Library

[12]

Soheib Baarir, Marco Beccuti, Davide Cerotti, Massimiliano De Pierro, Susanna Donatelli, and Giuliana Franceschinis. 2009. The GreatSPN tool: Recent enhancements. SIGMETRICS Perform. Eval. Rev. 36, 4 (March 2009), 4--9.

Digital Library

[13]

Francis Bacon. 1902. Novum Organum. P. F. Collier 8 Sons.

[14]

Christel Baier, Boudewijn Haverkort, Holger Hermanns, and Joost-Pieter Katoen. 2003. Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Softw. Eng. 29, 6 (June 2003), 524--541.

Digital Library

[15]

Paolo Ballarini, Benoît Barbot, Marie Duflot, Serge Haddad, and Nihal Pekergin. 2015. HASL: A new approach for performance evaluation and model checking from concepts to experimentation. Perform. Eval. 90 (2015), 53--77.

Digital Library

[16]

Benoît Barbot, Serge Haddad, and Claudine Picaronny. 2012. Coupling and importance sampling for statistical model checking. In Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’12), Cormac Flanagan and Barbara König (Eds.). Springer, Berlin, Germany, 331--346.

Digital Library

[17]

Samik Basu, Arka P. Ghosh, and Ru He. 2009. Approximate model checking of PCTL involving unbounded path properties. In Proceedings of the 11th International Conference on Formal Engineering Methods and Software Engineering (ICFEM’09), Karin Breitman and Ana Cavalcanti (Eds.). Springer, Berlin, Germany, 326--346.

Digital Library

[18]

Marco Beccuti and Giuliana Franceschinis. 2012. Efficient simulation of stochastic well-formed nets through symmetry exploitation. In Proceedings of the Winter Simulation Conference (WSC’12). Winter Simulation Conference, Article 296, 13 pages.

Digital Library

[19]

Jonathan Bogdoll, Luis María Ferrer Fioriti, Arnd Hartmanns, and Holger Hermanns. 2011. Partial order methods for statistical model checking and simulation. In Proceedings of the Joint 13th International Conference on Formal Techniques for Distributed Systems (FMOODS’11) and 30th IFIP WG 6.1 International Conference (FORTE’11), Roberto Bruni and Juergen Dingel (Eds.). Springer, Berlin, Germany, 59--74.

Digital Library

[20]

Jonathan Bogdoll, Arnd Hartmanns, and Holger Hermanns. 2012. Simulation and statistical model checking for modestly nondeterministic models. In Proceedings of the 16th International GI/ITG Conference on Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance (MMB 8 DFT’12), Jens B. Schmitt (Ed.). Springer, Berlin, Germany, 249--252.

Digital Library

[21]

Dimitri Bohlender, Harold Bruintjes, Sebastian Junges, Jens Katelaan, Viet Yen Nguyen, and Thomas Noll. 2014. A review of statistical model checking pitfalls on real-time stochastic models. In Proceedings of the 6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications (ISoLA’14), Tiziana Margaria and Bernhard Steffen (Eds.). Springer, Berlin, Germany, 177--192.

[22]

Henrik Bohnenkamp, Pedro R. D’Argenio, Holger Hermanns, and Joost-Pieter Katoen. 2006. MODEST: A compositional modeling formalism for hard and softly timed systems. IEEE Trans. Softw. Eng. 32, 10 (Oct 2006), 812--830.

Digital Library

[23]

Alexandre Borghi, Thomas Hérault, Richard Lassaigne, and Sylvain Peyronnet. 2008. Cell assisted APMC. In Proceedings of the 5th International Conference on Quantitative Evaluation of Systems (QEST’08). 75--76.

Digital Library

[24]

Patricia Bouyer, Thomas Brihaye, and Nicolas Markey. 2006. Improved undecidability results on weighted timed automata. Inform. Process. Lett. 98, 5 (2006), 188--194.

Digital Library

[25]

Benoît Boyer, Kevin Corre, Axel Legay, and Sean Sedwards. 2013. PLASMA-lab: A flexible, distributable statistical model checking library. In Proceedings of the 10th International Conference on Quantitative Evaluation of Systems (QEST’13), Kaustubh Joshi, Markus Siegle, Mariëlle Stoelinga, and Pedro R. D’Argenio (Eds.). Springer, Berlin, Germany, 160--164.

Digital Library

[26]

Peter Bulychev, Alexandre David, Kim Guldstrand Larsen, Marius Mikučionis, Danny Bøgsted Poulsen, Axel Legay, and Zheng Wang. 2012. UPPAAL-SMC: Statistical model checking for priced timed automata. In Proceedings of the 10th Workshop on Quantitative Aspects of Programming Languages and Systems (Electronic Proceedings in Theoretical Computer Science), Herbert Wiklicky and Mieke Massink (Eds.), Vol. 85. Open Publishing Association, 1--16.

[27]

Michaël Cadilhac, Thomas Hérault, Richard Lassaigne, Sylvain Peyronnet, and Sébastien Tixeuil. 2007. Evaluating complex MAC protocols for sensor networks with APMC. Electron. Notes Theoret. Comput. Sci. 185 (2007), 33--46. Proceedings of the 6th International Workshop on Automated Verification of Critical Systems (AVoCS’06)

Digital Library

[28]

Francesco Calzolai and Michele Loreti. 2010. Simulation and analysis of distributed systems in klaim. In Proceedings of the 12th International Conference on Coordination Models and Languages (COORDINATION’10), Dave Clarke and Gul Agha (Eds.). Springer, Berlin, Germany, 122--136.

Digital Library

[29]

Quentin Cappart, Christophe Limbrée, Pierre Schaus, Jean Quilbeuf, Louis-Marie Traonouez, and Axel Legay. 2017. Verification of interlocking systems using statistical model checking. In Proceedings of the 2017 IEEE 18th International Symposium on High Assurance Systems Engineering (HASE’17). 61--68.

[30]

Frédéric Cérou and Arnaud Guyader. 2007. Adaptive multilevel splitting for rare event analysis. Stochast. Anal. Appl. 25, 2 (2007), 417--443.

[31]

Mounir Chadli, Jin Hyun Kim, Axel Legay, Louis-Marie Traonouez, Stefan Naujokat, Bernhard Steffen, and Kim Guldstrand Larsen. 2016. A model-based framework for the specification and analysis of hierarchical scheduling systems. In Proceedings of the Joint 21st International Workshop on Formal Methods for Industrial Critical Systems and 16th International Workshop on Automated Verification of Critical Systems (FMICS-AVoCS’16), Maurice H. ter Beek, Stefania Gnesi, and Alexander Knapp (Eds.). Springer International Publishing, Cham, 133--141.

[32]

Y. S. Chow and Herbert Robbins. 1965. On the asymptotic theory of fixed-width sequential confidence intervals for the mean. Ann. Math. Stat. 36, 2 (1965), 457--462.

[33]

Edmund M. Clarke, E. Allen Emerson, and Aravinda Prasad Sistla. 1986. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8, 2 (April 1986), 244--263.

Digital Library

[34]

Edmund M. Clarke, James R. Faeder, Christopher J. Langmead, Leonard A. Harris, Sumit Kumar Jha, and Axel Legay. 2008. Statistical model checking in biolab: Applications to the automated analysis of T-cell receptor signaling pathway. In Proceedings of the 6th International Conference on Computational Methods in Systems Biology (CMSB’08), Monika Heiner and Adelinde M. Uhrmacher (Eds.). Springer, Berlin, Germany, 231--250.

Digital Library

[35]

Edmund M. Clarke and Paolo Zuliani. 2011. Statistical model checking for cyber-physical systems. In Proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis (ATVA’11), Tevfik Bultan and Pao-Ann Hsiung (Eds.). Springer, Berlin, Germany, 1--12.

Digital Library

[36]

COSMOS. 2015. COSMOS tool. Retrieved from http://www.lsv.ens-cachan.fr/Software/cosmos/.

[37]

Przemysław Daca, Thomas A. Henzinger, Jan Křetínský, and Tatjana Petrov. 2016. Faster statistical model checking for unbounded temporal properties. In Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’16), Marsha Chechik and Jean-François Raskin (Eds.). Springer, Berlin, Germany, 112--129.

Digital Library

[38]

Pedro D’Argenio, Axel Legay, Sean Sedwards, and Louis-Marie Traonouez. 2015. Smart sampling for lightweight verification of Markov decision processes. Int. J. Softw. Tools Technol. Transfer 17, 4 (2015), 469--484.

Digital Library

[39]

Alexandre David, Dehui Du, Kim G. Larsen, Axel Legay, Marius Mikučionis, Danny Bøgsted Poulsen, and Sean Sedwards. 2012. Statistical model checking for stochastic hybrid systems. In Proceedings of the 1st International Workshop on Hybrid Systems and Biology (Electronic Proceedings in Theoretical Computer Science), Ezio Bartocci and Luca Bortolussi (Eds.), Vol. 92. Open Publishing Association, 122--136.

[40]

Alexandre David, Kim G. Larsen, Axel Legay, Guangyuan Li, and Danny Bøgsted Poulsen. 2014. Quantified dynamic metric temporal logic for dynamic networks of stochastic hybrid automata. In Proceedings of the 2014 14th International Conference on Application of Concurrency to System Design. 32--41.

Digital Library

[41]

Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikučionis, Danny Bøgsted Poulsen, Jonas Vliet, and Zheng Wang. 2011. Statistical model checking for networks of priced timed automata. In Proceedings of the 9th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS’11), Uli Fahrenberg and Stavros Tripakis (Eds.). Springer, Berlin, Germany, 80--96.

Digital Library

[42]

Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikučionis, and Zheng Wang. 2011. Time for statistical model checking of real-time systems. In Proceedings of the 23rd International Conference on Formal Modeling and Analysis of Timed Systems (CAV’11), Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer, Berlin, Germany, 349--355.

Digital Library

[43]

Marie Duflot, Laurent Fribourg, Thomas Herault, Richard Lassaigne, Frédéric Magniette, Stéphane Messika, Sylvain Peyronnet, and Claudine Picaronny. 2005. Probabilistic model checking of the CSMA/CD protocol using PRISM and APMC. Electron. Notes Theoret. Comput. Sci. 128, 6 (2005), 195--214. Proceedings of the 4th International Workshop on Automated Verification of Critical Systems (AVoCS’04)

Digital Library

[44]

Diana El Rabih and Nihal Pekergin. 2009. Statistical model checking using perfect simulation. In Proceedings of the 7th International Symposium on Automated Technology for Verification and Analysis (ATVA’09), Zhiming Liu and Anders P. Ravn (Eds.). Springer, Berlin, Germany, 120--134.

Digital Library

[45]

GreatSPN. 2012. GreatSPN tool. Retrieved from http://www.di.unito.it/greatspn/index.html.

[46]

Radu Grosu and Scott A. Smolka. 2005. Monte carlo model checking. In Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’05), Nicolas Halbwachs and Lenore D. Zuck (Eds.). Springer, Berlin, Germany, 271--286.

Digital Library

[47]

Stefan Hadjis and Stefano Ermon. 2015. Importance sampling over sets: A new probabilistic inference scheme. In Proceedings of the 31st Conference on Uncertainty in Artificial Intelligence, Marina Meila and Tom Heskes (Eds.). AUAI Press, Corvallis, OR, 355--364. Retrieved from http://auai.org/uai2015/proceedings/papers/143.pdf.

Digital Library

[48]

Hans Hansson and Bengt Jonsson. 1994. A logic for reasoning about time and reliability. Formal Aspects Comput. 6, 5 (1994), 512--535.

Digital Library

[49]

Klaus Havelund and Grigore Roşu. 2002. Synthesizing monitors for safety properties. In Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’02), Joost-Pieter Katoen and Perdita Stevens (Eds.). Springer, Berlin, Germany, 342--356.

Digital Library

[50]

Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. 2000. On the use of model checking techniques for dependability evaluation. In Proceedings of the 19th IEEE Symposium on Reliable Distributed Systems (SRDS’00). 228--237.

Digital Library

[51]

Monika Heiner, Christian Rohr, and Martin Schwarick. 2013. MARCIE—Model checking and reachability analysis done efficiently. In Proceedings of the 34th International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS’13), José-Manuel Colom and Jörg Desel (Eds.). Springer, Berlin, Germany, 389--399.

Digital Library

[52]

Monika Heiner, Christian Rohr, Martin Schwarick, and Stefan Streif. 2010. A comparative study of stochastic analysis techniques. In Proceedings of the 8th International Conference on Computational Methods in Systems Biology (CMSB’10). ACM, New York, NY, 96--106.

Digital Library

[53]

David Henriques, João G. Martins, Paolo Zuliani, André Platzer, and Edmund M. Clarke. 2012. Statistical model checking for markov decision processes. In Proceedings of the 2012 9th International Conference on Quantitative Evaluation of Systems (QEST’12). 84--93.

Digital Library

[54]

Thomas Hérault, Richard Lassaigne, Frédéric Magniette, and Sylvain Peyronnet. 2004. Approximate probabilistic model checking. In Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’04), Bernhard Steffen and Giorgio Levi (Eds.). Springer, Berlin, Germany, 73--84.

[55]

Thomas Hérault, Richard Lassaigne, and Sylvain Peyronnet. 2006. APMC 3.0: Approximate verification of discrete and continuous time markov chains. In Proceedings of the 3rd International Conference on the Quantitative Evaluation of Systems (QEST’06). 129--130.

Digital Library

[56]

Holger Hermanns, Joachim Meyer-Kayser, and Markus Siegle. 1999. Multi terminal binary decision diagrams to represent and analyse continuous time markov chains. In Proceedings of the 3rd International Workshop on the Numerical Solution of Markov Chains. 188--207.

[57]

Wassily Hoeffding. 1963. Probability inequalities for sums of bounded random variables. J. Amer. Stat. Assoc. 58, 301 (1963), 13--30.

[58]

Johannes Hölzl and Tobias Nipkow. 2012. Verifying pCTL model checking. In Proceedings of the18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’12), Cormac Flanagan and Barbara König (Eds.). Springer, Berlin, Germany, 347--361.

Digital Library

[59]

Oliver C. Ibe and Kishor S. Trivedi. 1990. Stochastic Petri net models of polling systems. IEEE J. Select. Areas Commun. 8, 9 (Dec 1990), 1649--1657.

Digital Library

[60]

Raj Jain. 1991. The Art of Computer Systems Performance Analysis: Techniques for Experimental Design, Measurement, Simulation, and Modeling. Wiley, Hoboken, NJ.

[61]

David N. Jansen, Joost-Pieter Katoen, Marcel Oldenkamp, Mariëlle Stoelinga, and Ivan Zapreev. 2008. How fast and fat is your probabilistic model checker? An experimental performance comparison. In Hardware and Software: Verification and Testing, Karen Yorav (Ed.). Lecture Notes in Computer Science, Vol. 4899. Springer, Berlin, Germany, 69--85.

Digital Library

[62]

Cyrille Jegourel, Axel Legay, and Sean Sedwards. 2013. Importance splitting for statistical model checking rare properties. In Proceedings of the 25th International Conference on Computer Aided Verification (CAV’13), Natasha Sharygina and Helmut Veith (Eds.). Springer, Berlin, Germany, 576--591.

[63]

Cyrille Jegourel, Axel Legay, and Sean Sedwards. 2014. An effective heuristic for adaptive importance splitting in statistical model checking. In Proceedings of the 6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications (ISoLA’14), Tiziana Margaria and Bernhard Steffen (Eds.). Springer, Berlin, Germany, 143--159.

[64]

Cyrille Jegourel, Axel Legay, and Sean Sedwards. 2016. Command-based importance sampling for statistical model checking. Theoret. Comput. Sci. 649 (2016), 1--24.

Digital Library

[65]

Sumit K. Jha, Edmund M. Clarke, Christopher J. Langmead, Axel Legay, André Platzer, and Paolo Zuliani. 2009. A Bayesian approach to model checking biological systems. In Proceedings of the 7th International Conference on Computational Methods in Systems Biology (CMSB’09), Pierpaolo Degano and Roberto Gorrieri (Eds.). Springer, Berlin, Germany, 218--234.

Digital Library

[66]

Sumit Kumar Jha and Christopher James Langmead. 2012. Exploring behaviors of stochastic differential equation models of biological systems using change of measures. BMC Bioinfo. 13, 5 (12 Apr 2012), S8.

[67]

Kenan Kalajdzic, Cyrille Jegourel, Anna Lukina, Ezio Bartocci, Axel Legay, Scott A. Smolka, and Radu Grosu. 2016. Feedback control for statistical model checking of cyber-physical systems. In Proceedings of the 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques (ISoLA’16), Tiziana Margaria and Bernhard Steffen (Eds.). Springer International Publishing, Cham, 46--61.

[68]

Vijay Anand Korthikanti, Mahesh Viswanathan, Gul Agha, and YoungMin Kwon. 2010. Reasoning about MDPs as transformers of probability distributions. In Proceedings of the 7th International Conference on the Quantitative Evaluation of Systems (QEST’10). 199--208.

Digital Library

[69]

Marta Kwiatkowska, Gethin Norman, and David Parker. 2011. PRISM 4.0: Verification of probabilistic real-time systems. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV’11), Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer, Berlin, Germany, 585--591.

Digital Library

[70]

Youngmin Kwon and Gul Agha. 2011. Verifying the evolution of probability distributions governed by a DTMC. IEEE Trans. Softw. Eng. 37, 1 (Jan 2011), 126--141.

Digital Library

[71]

Youngmin Kwon and Gul Agha. 2013. Performance evaluation of sensor networks by statistical modeling and euclidean model checking. ACM Trans. Sen. Netw. 9, 4, Article 39 (July 2013), 38 pages.

Digital Library

[72]

David Kyle, Jeffery Hansen, and Sagar Chaki. 2015. Statistical model checking of distributed adaptive real-time software. In Proceedings of the 6th International Conference on Runtime Verification (RV’15), Ezio Bartocci and Rupak Majumdar (Eds.). Springer International Publishing, Cham, 269--274.

[73]

Tze Leung Lai. 2001. Sequential analysis: Some classical problems and new challenges. Statistica Sinica 11, 2 (2001), 303--351.

[74]

Kim G. Larsen and Arne Skou. 1991. Bisimulation through probabilistic testing. Info. Comput. 94, 1 (1991), 1--28.

Digital Library

[75]

Richard Lassaigne and Sylvain Peyronnet. 2002. Approximate verification of probabilistic systems. In Proceedings of the 2nd Joint International Workshop on Process Algebra and Probabilistic Methods: Performance Modeling and Verification (PAPM-PROBMIV’02), Holger Hermanns and Roberto Segala (Eds.). Springer, Berlin, Germany, 213--214.

Digital Library

[76]

Richard Lassaigne and Sylvain Peyronnet. 2008. Probabilistic verification and approximation. Ann. Pure Appl. Logic 152, 13 (2008), 122--131. Proceedings of the 12th Workshop on Logic, Language, Information and Computation

[77]

Richard Lassaigne and Sylvain Peyronnet. 2015. Approximate planning and verification for large Markov decision processes. Int. J. Softw. Tools Technol. Transfer 17, 4 (2015), 457--467.

Digital Library

[78]

Pierre L’Ecuyer, Valérie Demers, and Bruno Tuffin. 2007. Rare events, splitting, and quasi-monte carlo. ACM Trans. Model. Comput. Simul. 17, 2, Article 9 (April 2007).

Digital Library

[79]

Axel Legay, Sean Sedwards, and Louis-Marie Traonouez. 2015. Scalable verification of Markov decision processes. In Proceedings of the Workshops: HOFM, SAFOME, OpenCert, MoKMaSD, and WS-FMDS, Carlos Canal and Akram Idani (Eds.). Springer International Publishing, Cham, 350--362.

[80]

Axel Legay, Sean Sedwards, and Louis-Marie Traonouez. 2016. Rare events for statistical model checking an overview. In Proceedings of the 10th International Workshop on Reachability Problems (RP’16), Kim Guldstrand Larsen, Igor Potapov, and Jiří Srba (Eds.). Springer International Publishing, Cham, 23--35.

[81]

Axel Legay and Louis-Marie Traonouez. 2016. Statistical model checking with change detection. In Transactions on Foundations for Mastering Change I, Bernhard Steffen (Ed.). Springer International Publishing, Cham, 157--179.

[82]

Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM 52, 7 (2009), 107--115.

Digital Library

[83]

Dennis V. Lindley. 1997. The choice of sample size. J. Roy. Stat. Soc. Ser. D (The Statistician) 46, 2 (1997), 129--138.

[84]

Si Liu, Son Nguyen, Jatin Ganhotra, Muntasir Raihan Rahman, Indranil Gupta, and José Meseguer. 2015. Quantitative analysis of consistency in NoSQL key-value stores. In Proceedings of the 12th International Conference on Quantitative Evaluation of Systems (QEST’15), Javier Campos and R. Boudewijn Haverkort (Eds.). Springer International Publishing, Cham, 228--243.

Digital Library

[85]

Anna Lukina, Lukas Esterle, Christian Hirsch, Ezio Bartocci, Junxing Yang, Ashish Tiwari, Scott A. Smolka, and Radu Grosu. 2017. ARES: Adaptive receding-horizon synthesis of optimal plans. In Proceedings of the 23rd International Conference on Quantitative Evaluation of Systems (TACAS’17), Axel Legay and Tiziana Margaria (Eds.). Springer, Berlin, Germany, 286--302.

Digital Library

[86]

Oded Maler. 2016. Some thoughts on runtime verification. In Proceedings of the 16th International Conference, on Runtime Verification (RV’16), Yliès Falcone and César Sánchez (Eds.). Springer International Publishing, Cham, 3--14.

[87]

MARCIE. 2017. MARCIE tool. Retrieved from http://www-dssz.informatik.tu-cottbus.de/DSSZ/Software/Marcie.

[88]

João Martins, André Platzer, and João Leite. 2011. Statistical model checking for distributed probabilistic-control hybrid automata with smart grid applications. In Proceedings of the 13th International Conference on Formal Engineering Methods and Software Engineering (ICFEM’11), Shengchao Qin and Zongyan Qiu (Eds.). Springer, Berlin, Germany, 131--146.

Digital Library

[89]

José Meseguer and Raman Sharykin. 2006. Specification and analysis of distributed object-based stochastic hybrid systems. In Proceedings of the 9th International Workshop on Hybrid Systems: Computation and Control (HSCC’06), João P. Hespanha and Ashish Tiwari (Eds.). Springer, Berlin, Germany, 460--475.

Digital Library

[90]

MODES. 2006. MODES tool. Retrieved from http://www.modestchecker.net.

[91]

MRMC. 2011. MRMC tool. Retrieved from http://www.mrmc-tool.org.

[92]

MultiVESTA. 2015. MultiVESTA tool. Retrieved from http://sysma.imtlucca.it/tools/multivesta/.

[93]

NIST. 2017. NIST/SEMATECH e-Handbook of Statistical Methods. Retrieved from http://www.itl.nist.gov/div898/handbook/ppc/section3/ppc333.htm.

[94]

Ayoub Nouri, Saddek Bensalem, Marius Bozga, Benoît Delahaye, Cyrille Jegourel, and Axel Legay. 2014. Statistical model checking QoS properties of systems with SBIP. Int. J. Softw. Tools Technol. Transfer 17, 2 (2014), 171--185.

Digital Library

[95]

Sucheendra K. Palaniappan, Benjamin M. Gyori, Bing Liu, David Hsu, and P. S. Thiagarajan. 2013. Statistical model checking based calibration and analysis of bio-pathway models. In Proceedings of the 11th International Conference on Computational Methods in Systems Biology (CMSB’13), Ashutosh Gupta and Thomas A. Henzinger (Eds.). Springer, Berlin, Germany, 120--134.

Digital Library

[96]

Danhua Peng, Roland Ewald, and Adelinde M. Uhrmacher. 2014. Towards semantic model composition via experiments. In Proceedings of the 2nd ACM SIGSIM Conference on Principles of Advanced Discrete Simulation (SIGSIM PADS’14). ACM, New York, NY, 151--162.

Digital Library

[97]

A. G. Phatak and N. M. Bhatt. 1967. Estimation of the fraction defective in curtailed sampling plans by attributes. Technometrics 9, 2 (1967), 219--228.

[98]

PLASMA. 2015. PLASMA Lab. Retrieved from http://project.inria.fr/plasma-lab/.

[99]

Karl Popper. 1968. Conjectures and Refutations: The Growth of Scientific Knowledge. Harper Torchbooks.

[100]

PRISM. 2017. PRISM Statistical Model Checker. Retrieved from http://www.prismmodelchecker.org/manual/RunningPRISM/StatisticalModelChecking.

[101]

James Gary Propp and David Bruce Wilson. 1996. Exact sampling with coupled markov chains and applications to statistical mechanics. Rand. Struct. Algor. 9, 1--2 (Aug. 1996), 223--252.

Digital Library

[102]

PVESTA. 2011. PVESTA tool. Retrieved from http://maude.cs.uiuc.edu/tools/pvesta/.

[103]

Jean Quilbeuf, Everton Cavalcante, Louis-Marie Traonouez, Flavio Oquendo, Thais Batista, and Axel Legay. 2016. A logic for the statistical model checking of dynamic software architectures. In Proceedings of the 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques (ISoLA’16), Tiziana Margaria and Bernhard Steffen (Eds.). Springer International Publishing, Cham, 806--820.

[104]

Daniël Reijsbergen, Pieter-Tjerk de Boer, Werner Scheinhardt, and Boudewijn Haverkort. 2010. Rare event simulation for highly dependable systems with fast repairs. In Proceedings of the 2010 7th International Conference on the Quantitative Evaluation of Systems. 251--260.

Digital Library

[105]

Nima Roohi and Mahesh Viswanathan. 2015. Statistical model checking for unbounded until formulas. Int. J. Softw. Tools Technol. Transfer 17, 4 (2015), 417--427.

Digital Library

[106]

SAM. 2010. SAM: Stochastic Analyser for Mobility. Retrieved from http://rap.dsi.unifi.it/SAM/.

[107]

Sriram Sankaranarayanan and Georgios Fainekos. 2012. Simulating insulin infusion pump risks by in-silico modeling of the insulin-glucose regulatory system. In Proceedings of the 10th International Conference on Computational Methods in Systems Biology (CMSB’12), David Gilbert and Monika Heiner (Eds.). Springer, Berlin, Germany, 322--341.

Digital Library

[108]

SBIP. 2013. SBIP tool. Retrieved from http://www-verimag.imag.fr/Statistical-Model-Checking.html.

[109]

Stefano Sebastio and Andrea Vandin. 2013. MultiVeStA: Statistical model checking for discrete event simulators. In Proceedings of the 7th International Conference on Performance Evaluation Methodologies and Tools (ValueTools’13). ICST (Institute for Computer Sciences, Social-Informatics and Telecommunications Engineering), ICST, Brussels, Belgium, 310--315.

Digital Library

[110]

Koushik Sen, Abhay Vardhan, Gul Agha, and Grigore Roşu. 2004. Efficient decentralized monitoring of safety in distributed systems. In Proceedings of the 26th International Conference on Software Engineering. 418--427.

Digital Library

[111]

Koushik Sen, Mahesh Viswanathan, and Gul Agha. 2004. Statistical model checking of black-box probabilistic systems. In Computer Aided Verification, Rajeev Alur and Doron A. Peled (Eds.). Lecture Notes in Computer Science, Vol. 3114. Springer, Berlin, Germany, 202--215.

[112]

Koushik Sen, Mahesh Viswanathan, and Gul Agha. 2005. On statistical model checking of stochastic systems. In Computer Aided Verification, Kousha Etessami and Sriram K. Rajamani (Eds.). Lecture Notes in Computer Science, Vol. 3576. Springer, Berlin, Germany, 266--280.

Digital Library

[113]

Koushik Sen, Mahesh Viswanathan, and Gul Agha. 2005. VESTA: A statistical model-checker and analyzer for probabilistic systems. Proceedings of the International Conference on Quantitative Evaluation of Systems. 251--252.

Digital Library

[114]

Koushik Sen, Mahesh Viswanathan, and Gul Agha. 2006. Model-checking markov chains in the presence of uncertainties. In Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’06), Holger Hermanns and Jens Palsberg (Eds.). Springer, Berlin, Germany, 394--410.

Digital Library

[115]

Rajan Srinivasan. 2002. Importance Sampling. Springer, Berlin, Germany.

[116]

Lisa J. Strug, Charles A. Rohde, and Paul N. Corey. 2007. An introduction to evidential sample size calculations. Amer. Stat. 61, 3 (2007), 207--212. Retrieved from http://www.jstor.org/stable/27643895.

[117]

Alexander Tartakovsky, Igor Nikiforov, and Michèle Basseville. 2014. Sequential Analysis: Hypothesis Testing and Changepoint Detection. Chapman and Hall/CRC, Boca Raton, FL.

[118]

Philip S. Thomas and Emma Brunskill. 2017. Importance sampling with unequal support. In Proceedings of the 31st AAAI Conference on Artificial Intelligence (AAAI’17). AAAI Press, Palo Alto, CA. Retrieved from https://aaai.org/ocs/index.php/AAAI/AAAI17/paper/view/14957/14457.

[119]

Kishor S. Trivedi. 2008. Probability 8 Statistics With Reliability, Queuing And Computer Science Applications (2nd ed.). Wiley, Hoboken, NJ.

Digital Library

[120]

UPPAAL 2015. UPPAAL. Retrieved from http://www.uppaal.org.

[121]

Abraham Wald. 1945. Sequential tests of statistical hypotheses. Ann. Math. Stat. 16, 2 (1945), 117--186.

[122]

Abraham Wald. 1950. Statistical Decision Functions. Wiley, New York, NY.

[123]

Abraham Wald. 1992. Breakthroughs in Statistics: Foundations and Basic Theory. Springer New York, New York, NY, Chapter Sequential Tests of Statistical Hypotheses, 256--298.

[124]

D. J. White. 1993. A survey of applications of markov decision processes. J. Oper. Res. Soc. 44, 11 (1993), 1073--1096.

[125]

Ymer. 2015. Ymer tool. Retrieved from http://www.tempastic.org/ymer/.

[126]

Håkan L. S. Younes. 2005. Probabilistic verification for “black-box” systems. In Computer Aided Verification, Kousha Etessami and Sriram K. Rajamani (Eds.). Lecture Notes in Computer Science, Vol. 3576. Springer, Berlin, Germany, 253--265.

Digital Library

[127]

Håkan L. S. Younes. 2005. Ymer: A statistical model checker. In Computer Aided Verification, Kousha Etessami and Sriram K. Rajamani (Eds.). Lecture Notes in Computer Science, Vol. 3576. Springer, Berlin, Germany, 429--433.

Digital Library

[128]

Håkan L. S. Younes. 2006. Error control for probabilistic model checking. In Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’06), E. Allen Emerson and Kedar S. Namjoshi (Eds.). Springer, Berlin, Germany, 142--156.

Digital Library

[129]

Håkan L. S. Younes, Edmund M. Clarke, and Paolo Zuliani. 2011. Statistical verification of probabilistic properties with unbounded until. In Proceedings of the 13th Brazilian Symposium on Formal Methods: Foundations and Applications (SBMF’10). Springer, Berlin, Germany, 144--160.

Digital Library

[130]

Håkan L. S. Younes, Marta Kwiatkowska, Gethin Norman, and David Parker. 2006. Numerical vs. statistical probabilistic model checking. Int. J. Softw. Tools Technol. Transfer 8, 3 (2006), 216--228.

Digital Library

[131]

Håkan L. S. Younes and Reid G. Simmons. 2002. Probabilistic verification of discrete event systems using acceptance sampling. In Computer Aided Verification, Ed Brinksma and Kim Guldstrand Larsen (Eds.). Lecture Notes in Computer Science, Vol. 2404. Springer, Berlin, Germany, 223--235.

Digital Library

[132]

Håkan L. S. Younes and Reid G. Simmons. 2006. Statistical probabilistic model checking with a focus on time-bounded properties. Info. Comput. 204, 9 (2006), 1368--1409.

Digital Library

[133]

Paolo Zuliani. 2015. Statistical model checking for biological applications. Int. J. Softw. Tools Technol. Transfer 17, 4 (2015), 527--536.

Digital Library

[134]

Paolo Zuliani, André Platzer, and Edmund M. Clarke. 2013. Bayesian statistical model checking with application to stateflow/simulink verification. Formal Methods Syst. Design 43, 2 (2013), 338--367.

Digital Library

Cited By

Nigro LCicirelli F(2024)Correctness Verification of Mutual Exclusion Algorithms by Model CheckingModelling10.3390/modelling50300375:3(694-719)Online publication date: 28-Jun-2024
https://doi.org/10.3390/modelling5030037
Nigro LCicirelli F(2024)Formal Modeling and Verification of Embedded Real-Time Systems: An Approach and Practical Tool Based on Constraint Time Petri NetsMathematics10.3390/math1206081212:6(812)Online publication date: 10-Mar-2024
https://doi.org/10.3390/math12060812
Han DMa GZhang XCai YLi A(2024)Rule Conflict Classification and Detection for Smart Building Systems: A Case Study2024 43rd Chinese Control Conference (CCC)10.23919/CCC63176.2024.10661964(5153-5158)Online publication date: 28-Jul-2024
https://doi.org/10.23919/CCC63176.2024.10661964
Show More Cited By

Index Terms

A Survey of Statistical Model Checking
1. Mathematics of computing
  1. Probability and statistics
    1. Probabilistic inference problems
      1. Hypothesis testing and confidence interval computation
    2. Statistical paradigms
2. Theory of computation
  1. Logic
    1. Verification by model checking

Recommendations

Bayesian statistical model checking with application to Stateflow/Simulink verification

We address the problem of model checking stochastic systems, i.e., checking whether a stochastic system satisfies a certain temporal property with a probability greater (or smaller) than a fixed threshold. In particular, we present a Statistical Model ...
Statistical probabilistic model checking with a focus on time-bounded properties

Probabilistic verification of continuous-time stochastic processes has received increasing attention in the model-checking community in the past 5 years, with a clear focus on developing numerical solution methods for model checking of continuous-time ...
Numerical vs. statistical probabilistic model checking

Numerical analysis based on uniformisation and statistical techniques based on sampling and simulation are two distinct approaches for transient analysis of stochastic systems. We compare the two solution techniques when applied to the verification of ...

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Modeling and Computer Simulation

ACM Transactions on Modeling and Computer Simulation Volume 28, Issue 1

January 2018

163 pages

ISSN:1049-3301

EISSN:1558-1195

DOI:10.1145/3174299

Editor:
Adelinde M. Uhrmacher
University of Rostock, Germany

Issue’s Table of Contents

Copyright © 2018 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 31 January 2018

Accepted: 01 November 2017

Revised: 01 September 2017

Received: 01 February 2017

Published in TOMACS Volume 28, Issue 1

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

NSF
AFOSR

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

204
Total Citations
View Citations
3,374
Total Downloads

Downloads (Last 12 months)569
Downloads (Last 6 weeks)66

Reflects downloads up to 04 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Nigro LCicirelli F(2024)Correctness Verification of Mutual Exclusion Algorithms by Model CheckingModelling10.3390/modelling50300375:3(694-719)Online publication date: 28-Jun-2024
https://doi.org/10.3390/modelling5030037
Nigro LCicirelli F(2024)Formal Modeling and Verification of Embedded Real-Time Systems: An Approach and Practical Tool Based on Constraint Time Petri NetsMathematics10.3390/math1206081212:6(812)Online publication date: 10-Mar-2024
https://doi.org/10.3390/math12060812
Han DMa GZhang XCai YLi A(2024)Rule Conflict Classification and Detection for Smart Building Systems: A Case Study2024 43rd Chinese Control Conference (CCC)10.23919/CCC63176.2024.10661964(5153-5158)Online publication date: 28-Jul-2024
https://doi.org/10.23919/CCC63176.2024.10661964
Jeon SCho KKang CLee JOh HKang J(2024)Quantum Probabilistic Model Checking for Time-Bounded PropertiesProceedings of the ACM on Programming Languages10.1145/36897318:OOPSLA2(557-587)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689731
Uhrmacher AFrazier PHähnle RKlügl FLorig FLudäscher BNenzi LRuiz-Martin CRumpe BSzabo CWainer GWilsdorf P(2024)Context, Composition, Automation, and Communication: The C2AC Roadmap for Modeling and SimulationACM Transactions on Modeling and Computer Simulation10.1145/367322634:4(1-51)Online publication date: 13-Aug-2024
https://dl.acm.org/doi/10.1145/3673226
Esposito MMancini TTronci E(2024)Optimizing Fault-Tolerant Quality-Guaranteed Sensor Deployments for UAV Localization in Critical Areas via Computational GeometryIEEE Transactions on Systems, Man, and Cybernetics: Systems10.1109/TSMC.2023.332743254:3(1515-1526)Online publication date: Mar-2024
https://doi.org/10.1109/TSMC.2023.3327432
Bu HSun M(2024)Clopper-Pearson Algorithms for Efficient Statistical Model Checking EstimationIEEE Transactions on Software Engineering10.1109/TSE.2024.3392720(1-20)Online publication date: 2024
https://doi.org/10.1109/TSE.2024.3392720
Zhao YHoxha BFainekos GDeshmukh JLindemann L(2024)Robust Conformal Prediction for STL Runtime Verification under Distribution Shift2024 ACM/IEEE 15th International Conference on Cyber-Physical Systems (ICCPS)10.1109/ICCPS61052.2024.00022(169-179)Online publication date: 13-May-2024
https://doi.org/10.1109/ICCPS61052.2024.00022
Tavolato PLuh REresheim SGmeiner SSchrittwieser S(2024)Quantifying the Odds in Real World Attack Scenarios2024 IEEE International Conference on Cyber Security and Resilience (CSR)10.1109/CSR61664.2024.10679461(845-852)Online publication date: 2-Sep-2024
https://doi.org/10.1109/CSR61664.2024.10679461
Mangi FSu GZhang M(2024)Advancing verification of process mining models with quantitative model checking in stochastic environmentITM Web of Conferences10.1051/itmconf/2024600001260(00012)Online publication date: 9-Jan-2024
https://doi.org/10.1051/itmconf/20246000012
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents