Gul Agha
Karl Palmskog
Skip Abstract Section
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.
- 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.Google Scholar
Cross Ref
- C. J. Adcock. 1997. Sample size determination: A review. J. Roy. Stat. Soci. Ser. D (The Statistician) 46, 2 (1997), 261--283.Google ScholarCross Ref
- 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.Google ScholarCross Ref
- 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).Google Scholar
- 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) Google ScholarDigital Library
- 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. Google ScholarDigital Library
- APMC. 2005. APMC2 tool. Retrieved from http://berbiqui.org/apmc2/apmc-2.0.0.tar.gz.Google Scholar
- APMCBeta. 2014. APMC3 Beta tool. Retrieved from https://web.archive.org/web/20140928144328http://sylvain.berbiqui.org/apmc.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Francis Bacon. 1902. Novum Organum. P. F. Collier 8 Sons.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Patricia Bouyer, Thomas Brihaye, and Nicolas Markey. 2006. Improved undecidability results on weighted timed automata. Inform. Process. Lett. 98, 5 (2006), 188--194. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 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) Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- Frédéric Cérou and Arnaud Guyader. 2007. Adaptive multilevel splitting for rare event analysis. Stochast. Anal. Appl. 25, 2 (2007), 417--443.Google ScholarCross Ref
- 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.Google ScholarCross Ref
- 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.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- COSMOS. 2015. COSMOS tool. Retrieved from http://www.lsv.ens-cachan.fr/Software/cosmos/.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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) Google ScholarDigital Library
- 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. Google ScholarDigital Library
- GreatSPN. 2012. GreatSPN tool. Retrieved from http://www.di.unito.it/greatspn/index.html.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Hans Hansson and Bengt Jonsson. 1994. A logic for reasoning about time and reliability. Formal Aspects Comput. 6, 5 (1994), 512--535.Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 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.Google Scholar
- Wassily Hoeffding. 1963. Probability inequalities for sums of bounded random variables. J. Amer. Stat. Assoc. 58, 301 (1963), 13--30.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Raj Jain. 1991. The Art of Computer Systems Performance Analysis: Techniques for Experimental Design, Measurement, Simulation, and Modeling. Wiley, Hoboken, NJ.Google Scholar
- 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. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 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.Google ScholarCross Ref
- Cyrille Jegourel, Axel Legay, and Sean Sedwards. 2016. Command-based importance sampling for statistical model checking. Theoret. Comput. Sci. 649 (2016), 1--24. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google Scholar
- 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.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- Tze Leung Lai. 2001. Sequential analysis: Some classical problems and new challenges. Statistica Sinica 11, 2 (2001), 303--351.Google Scholar
- Kim G. Larsen and Arne Skou. 1991. Bisimulation through probabilistic testing. Info. Comput. 94, 1 (1991), 1--28. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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 ComputationGoogle ScholarCross Ref
- 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. Google ScholarDigital Library
- 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). Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 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.Google ScholarCross Ref
- 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.Google Scholar
- Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM 52, 7 (2009), 107--115. Google ScholarDigital Library
- Dennis V. Lindley. 1997. The choice of sample size. J. Roy. Stat. Soc. Ser. D (The Statistician) 46, 2 (1997), 129--138.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- MARCIE. 2017. MARCIE tool. Retrieved from http://www-dssz.informatik.tu-cottbus.de/DSSZ/Software/Marcie.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- MODES. 2006. MODES tool. Retrieved from http://www.modestchecker.net.Google Scholar
- MRMC. 2011. MRMC tool. Retrieved from http://www.mrmc-tool.org.Google Scholar
- MultiVESTA. 2015. MultiVESTA tool. Retrieved from http://sysma.imtlucca.it/tools/multivesta/.Google Scholar
- NIST. 2017. NIST/SEMATECH e-Handbook of Statistical Methods. Retrieved from http://www.itl.nist.gov/div898/handbook/ppc/section3/ppc333.htm.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- PLASMA. 2015. PLASMA Lab. Retrieved from http://project.inria.fr/plasma-lab/.Google Scholar
- Karl Popper. 1968. Conjectures and Refutations: The Growth of Scientific Knowledge. Harper Torchbooks.Google Scholar
- PRISM. 2017. PRISM Statistical Model Checker. Retrieved from http://www.prismmodelchecker.org/manual/RunningPRISM/StatisticalModelChecking.Google Scholar
- 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. Google ScholarDigital Library
- PVESTA. 2011. PVESTA tool. Retrieved from http://maude.cs.uiuc.edu/tools/pvesta/.Google Scholar
- 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.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- Nima Roohi and Mahesh Viswanathan. 2015. Statistical model checking for unbounded until formulas. Int. J. Softw. Tools Technol. Transfer 17, 4 (2015), 417--427. Google ScholarDigital Library
- SAM. 2010. SAM: Stochastic Analyser for Mobility. Retrieved from http://rap.dsi.unifi.it/SAM/.Google Scholar
- 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. Google ScholarDigital Library
- SBIP. 2013. SBIP tool. Retrieved from http://www-verimag.imag.fr/Statistical-Model-Checking.html.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Rajan Srinivasan. 2002. Importance Sampling. Springer, Berlin, Germany.Google Scholar
- 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.Google ScholarCross Ref
- Alexander Tartakovsky, Igor Nikiforov, and Michèle Basseville. 2014. Sequential Analysis: Hypothesis Testing and Changepoint Detection. Chapman and Hall/CRC, Boca Raton, FL. Google ScholarCross Ref
- 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.Google Scholar
- Kishor S. Trivedi. 2008. Probability 8 Statistics With Reliability, Queuing And Computer Science Applications (2nd ed.). Wiley, Hoboken, NJ. Google ScholarDigital Library
- UPPAAL 2015. UPPAAL. Retrieved from http://www.uppaal.org.Google Scholar
- Abraham Wald. 1945. Sequential tests of statistical hypotheses. Ann. Math. Stat. 16, 2 (1945), 117--186.Google ScholarCross Ref
- Abraham Wald. 1950. Statistical Decision Functions. Wiley, New York, NY.Google Scholar
- Abraham Wald. 1992. Breakthroughs in Statistics: Foundations and Basic Theory. Springer New York, New York, NY, Chapter Sequential Tests of Statistical Hypotheses, 256--298.Google Scholar
- D. J. White. 1993. A survey of applications of markov decision processes. J. Oper. Res. Soc. 44, 11 (1993), 1073--1096.Google ScholarCross Ref
- Ymer. 2015. Ymer tool. Retrieved from http://www.tempastic.org/ymer/.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Paolo Zuliani. 2015. Statistical model checking for biological applications. Int. J. Softw. Tools Technol. Transfer 17, 4 (2015), 527--536. Google ScholarDigital Library
- 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. Google ScholarDigital Library
Index Terms
- A Survey of Statistical 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