This page presents our Statistical Model Checking Extension for the UPPAAL Toolset! This new version of UPPAAL results from a collaboration between Aalborg University and INRIA Rennes.
What is Statistical Model Checking?
Statistical Model Checking (SMC) refers to a series of techniques that monitor several runs of the system with respect to some property, and then use results from the statistics to get an overall estimate of the correctness of the design. The approach has been applied to problems that are far beyond the scope of existing model checkers. In fact, SMC gets widely accepted in various research areas such as systems biology [JCLLPZ09, CFLHJL08] or software engineering [You05a], in particular for industrial applications [BBBCDL10]. There are several reasons for this success. First, it is very simple to implement, understand and use (especially by industry, software engineers, and generally all people that are not pure researchers but customers for our results and tools). Second, it requires little or no extra modeling or specification effort, but simply an operational model of the system that can be simulated and checked against properties. Third, the use of Statistics allows to approximate undecidable problems. Finally, it is possible to easily distribute SMC [BDLLMP12].
Why do we use Statistical Model Checking?
In a recent work [BDLLMPW11], we used the model of Priced Timed Automata (PTA), that are timed systems in which clocks may have different rates (even potentially negative) in different locations. Such automata are as expressive as linear hybrid automata or priced timed automata, but the addition of features such as input and output modalities allow us to specify complex problems in an elegant manner. Unfortunately most of such problems are either undecidable or too complex to be solved with classical model checking approaches (state-space explosion). Our solution:
- We define a stochastic semantic for CSTAs. This semantic is natural as it gives a stochastic meaning to timed behaviors. Moreover, it is preserved by composition.
- We apply SMC on the resulting stochastic timed system.
- Why is this different from Classical UPPAAL?
There are two major differences with classical UPPAAL: 1. the user interface allows to specify probability distributions that drive the timed behaviors, and 2. The engine offers a statistical model checking support capable of a) computing an estimate of a probability, b) compare a probability with a value, and c) compare two probabilities without computing them. Our engine relies on powerful results coming from the statistics such as sequential hypothesis testing, or monte carlo simulation.
Why are we better than other toolsets?
Classical SMC model checkers[ You05a, SVA05b, KZHHJ09] are either capable of computing an estimate of the probability or test whether this probability is greater or equal to some value. All those implementations are unable to handle timed systems. Moreover, contrary to those implementations, our tool also implements those tests that can compare two probabilities without computing them. Finally, contrary to other SMC-based tools, the UPPAAL extension comes with a wide range of functionalities that allows the user to visualize the results on the form of probability distributions, evolution of the number of runs with timed bounds, computation of expected values, ... There are other very rich framework for specifying stochastic timed systems. An example of such framework is the MoDeST [BDArHK04] toolset. Here, however, general hybrid variables are not considered and parallel composition do not yield fully stochastic models. For the notion of probabilistic hybrid systems considered in [HSCC11] the choice of time is resolved non-deterministically rather than stochastically as in our case and as required by SMC.
- [BDLLMP12] Peter Bulychev, Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikucionis, and Danny Bøgsted Poulsen. Checking & Distributing Statistical Model Checking. 4th NASA Formal Methods Symposium, 2012, pages 449-463, LNCS 7226, Springer.
- [JCLLPZ09] Sumit Kumar Jha, Edmund M. Clarke, Christopher James Langmead, Axel Legay, André Platzer, and Paolo Zuliani. A Bayesian Approach to Model Checking Biological Systems. In Proceedings of CMSB, pages 218-234, 2009, LNCS 5688, Springer.
- [CFLHJL08] Edmund M. Clarke, James R. Faeder, Christopher James Langmead, Leonard A. Harris, Sumit Kumar Jha, and Axel Legay. Statistical Model Checking in BioLab: Applications to the Automated Analysis of T-Cell Receptor Signaling Pathway. In Proceedings of CMSB, pages 231-250, 2008, LNCS, Springer.
- [You05a] H. L. S. Younes. Verification and Planning for Stochastic Processes with Asynchronous Events. Ph.D., Carnegie Mellon, 2005.
- [BBBCDL10] A. Basu, S. Bensalem, M. Bozga, B. Caillaud, B. Delahaye, and A. Legay. Statistical Abstraction and Model-Checking of Large Heterogeneous Systems. In Proceedings of FORTE, pages 32-46, 2010, LNCS 6117, Springer.
- [BDLLMPW11] Peter Bulychev, Alexandre David, Kim Guldstrand Larsen, Axel Legay, Marius Mikucionis, Danny Bøgsted Poulsen, and Zheng Wang. Statistical Model Checking for Priced Timed Automata. pdf.
- [SVA05b] K. Sen, M. Viswanathan, and G. A. Agha. VESTA: A Statistical Model-checker and Analyzer for Probabilistic Systems. In Proceedings of QEST 2005, pages 251-252. IEEE Computer Society.
- [KZHHJ09] J-Pieter Katoen, I. S. Zapreev, E. Moritz Hahn, H. Hermanns, and D. N. Jansen. The Ins and Outs of the Probabilistic Model Checker MRMC. In Proceedings of QUEST 2009, pages 167-176. IEEE Computer Society.
- [BDArHK04] H. Bohnenkamp, P.R. D'Argenio, H. Hermanns, and J.-P. Katoen. MoDeST: A compositional modeling formalism for real-time and stochastic systems. Technical report CTITT, 04-46, University of Twente, 2004.
- [HSCC11] Tino Teige, Andreas Eggers, and Martin Fränzle. Constraint-Based Analysis of Concurrent Probabilistic Hybrid Systems: An Application to Networked Automation Systems. In Nonlinear Analysis: Hybrid Systems, 2011.
Latest NewsVersion 4.1.4 released.
11 Jul 2011
The version of UPPAAL supporting the new statistical model-checker was released on the 11th of July. The development version on www.uppaal.org supports it.Version 4.1.4 announced.
20 Jan 2011
The next development of UPPAAL will include a statistical model-checker engine.