User menu

Accès à distance ? S'identifier sur le proxy UCLouvain

On the Power of Statistical Model Checking

Primary tabs

Larsen Kim, Guldstrand Legay, Axel [UCL]

This paper contains material for our tutorial presented at STRESS 2016. This includes an introduction to Statistical Model Checking algorithms and their rare event extensions, as well as an introduction to two well-known SMC tools: Plasma and Uppaal.

Document type Communication à un colloque (Conference Paper) – Présentation orale avec comité de sélection
Publication date 2016
Language Anglais
Conference "7th International Symposium, ISoLA 2016" (10/10/2016)
Peer reviewed yes
Host document "Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications Lecture Notes in Computer Science" (ISBN : 9783319471686)
Publisher Springer International Publishing (Cham)
Publication status Publié
Affiliation UCL - SST/ICTM/INGI - Pôle en ingénierie informatique
Links
  1. Alur R., Courcoubetis C., Dill D., Model-Checking in Dense Real-Time, 10.1006/inco.1993.1024
  2. Alur Rajeev, Dill David L., A theory of timed automata, 10.1016/0304-3975(94)90010-8
  3. Behrmann Gerd, Distributed reachability analysis in timed automata, 10.1007/s10009-003-0111-z
  4. Behrmann Gerd, Cougnard Agnès, David Alexandre, Fleury Emmanuel, Larsen Kim G., Lime Didier, UPPAAL-Tiga: Time for Playing Games!, Computer Aided Verification ISBN:9783540733676 p.121-125, 10.1007/978-3-540-73368-3_14
  5. Behrmann, G., David, A., Larsen, K.G., Håkansson, J., Pettersson, P., Yi, W., Hendriks, M.: Uppaal 4.0. In: QEST. IEEE Computer Society (2006)
  6. Behrmann Gerd, David Alexandre, Larsen Kim Guldstrand, Pettersson Paul, Yi Wang, Developing UPPAAL over 15 years, 10.1002/spe.1006
  7. David Alexandre, Behrmann Gerd, Larsen Kim G., Yi Wang, Unification & Sharing in Timed Automata Verification, Model Checking Software (2003) ISBN:9783540401179 p.225-229, 10.1007/3-540-44829-2_15
  8. Behrmann Gerd, Fehnker Ansgar, Hune Thomas, Larsen Kim, Pettersson Paul, Romijn Judi, Efficient Guiding Towards Cost-Optimality in UPPAAL, Tools and Algorithms for the Construction and Analysis of Systems (2001) ISBN:9783540418658 p.174-188, 10.1007/3-540-45319-9_13
  9. Behrmann Gerd, Fehnker Ansgar, Hune Thomas, Larsen Kim, Pettersson Paul, Romijn Judi, Vaandrager Frits, Minimum-Cost Reachability for Priced Time Automata, Hybrid Systems: Computation and Control (2001) ISBN:9783540418665 p.147-161, 10.1007/3-540-45351-2_15
  10. Behrmann Gerd, Hune Thomas, Vaandrager Frits, Distributing Timed Model Checking — How the Search Order Matters, Computer Aided Verification (2000) ISBN:9783540677703 p.216-231, 10.1007/10722167_19
  11. Behrmann G., Larsen K. G., Pearson J., Weise C., Yi W., Efficient Timed Reachability Analysis Using Clock Difference Diagrams, Computer Aided Verification (1999) ISBN:9783540662020 p.341-353, 10.1007/3-540-48683-6_30
  12. Boyer Benoît, Corre Kevin, Legay Axel, Sedwards Sean, PLASMA-lab: A Flexible, Distributable Statistical Model Checking Library, Quantitative Evaluation of Systems (2013) ISBN:9783642401954 p.160-164, 10.1007/978-3-642-40196-1_12
  13. Bulychev Peter, David Alexandre, Larsen Kim G., Legay Axel, Mikučionis Marius, Computing Nash Equilibrium in Wireless Ad Hoc Networks: A Simulation-Based Approach, 10.4204/eptcs.78.1
  14. Colombo Alessio, Fontanelli Daniele, Gandhi Dhaval, De Angeli Antonella, Palopoli Luigi, Sedwards Sean, Legay Axel, Behavioural templates improve robot motion planning with social force model in human environments, 10.1109/etfa.2013.6648081
  15. Colombo Alessio, Fontanelli Daniele, Legay Axel, Palopoli Luigi, Sedwards Sean, Motion planning in crowds using statistical model checking to enhance the social force model, 10.1109/cdc.2013.6760437
  16. David Alexandre, Jensen Peter G., Larsen Kim Guldstrand, Legay Axel, Lime Didier, Sørensen Mathias Grund, Taankvist Jakob H., On Time with Minimal Expected Cost!, Automated Technology for Verification and Analysis (2014) ISBN:9783319119359 p.129-145, 10.1007/978-3-319-11936-6_10
  17. David Alexandre, Jensen Peter Gjøl, Larsen Kim Guldstrand, Mikučionis Marius, Taankvist Jakob Haahr, Uppaal Stratego, Tools and Algorithms for the Construction and Analysis of Systems (2015) ISBN:9783662466803 p.206-211, 10.1007/978-3-662-46681-0_16
  18. David Alexandre, Larsen Kim G., Legay Axel, Mikučionis Marius, Schedulability of Herschel revisited using statistical model checking, 10.1007/s10009-014-0331-4
  19. David Alexandre, Larsen Kim Guldstrand, Legay Axel, Mikučionis Marius, Poulsen Danny Bøgsted, Sedwards Sean, Runtime Verification of Biological Systems, Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change (2012) ISBN:9783642340253 p.388-404, 10.1007/978-3-642-34026-0_29
  20. David Alexandre, Larsen Kim G., Legay Axel, Mikučionis Marius, Poulsen Danny Bøgsted, Sedwards Sean, Statistical model checking for biological systems, 10.1007/s10009-014-0323-4
  21. David Alexandre, Larsen Kim G., Legay Axel, Mikučionis Marius, Wang Zheng, Time for Statistical Model Checking of Real-Time Systems, Computer Aided Verification (2011) ISBN:9783642221095 p.349-355, 10.1007/978-3-642-22110-1_27
  22. David Alexandre, Möller M. Oliver, Yi Wang, Formal Verification of UML Statecharts with Real-Time Extensions, Fundamental Approaches to Software Engineering (2002) ISBN:9783540433538 p.218-232, 10.1007/3-540-45923-5_15
  23. Helbing Dirk, Molnár Péter, Social force model for pedestrian dynamics, 10.1103/physreve.51.4282
  24. Hendriks Martijn, Larsen Kim G., Exact Acceleration of Real-Time Model Checking, 10.1016/s1571-0661(04)80473-0
  25. Henzinger Thomas A., Ho Pei -Hsin, Algorithmic analysis of nonlinear hybrid systems, Computer Aided Verification (1995) ISBN:9783540600459 p.225-238, 10.1007/3-540-60045-0_53
  26. Hérault Thomas, Lassaigne Richard, Magniette Frédéric, Peyronnet Sylvain, Approximate Probabilistic Model Checking, Lecture Notes in Computer Science (2004) ISBN:9783540208037 p.73-84, 10.1007/978-3-540-24622-0_8
  27. Jegourel Cyrille, Legay Axel, Sedwards Sean, A Platform for High Performance Statistical Model Checking – PLASMA, Tools and Algorithms for the Construction and Analysis of Systems (2012) ISBN:9783642287558 p.498-503, 10.1007/978-3-642-28756-5_37
  28. Jegourel Cyrille, Legay Axel, Sedwards Sean, Cross-Entropy Optimisation of Importance Sampling Parameters for Statistical Model Checking, Computer Aided Verification (2012) ISBN:9783642314230 p.327-342, 10.1007/978-3-642-31424-7_26
  29. Jegourel Cyrille, Legay Axel, Sedwards Sean, Importance Splitting for Statistical Model Checking Rare Properties, Computer Aided Verification (2013) ISBN:9783642397981 p.576-591, 10.1007/978-3-642-39799-8_38
  30. Jégourel, C., Legay, A., Sedwards, S., Traonouez, L.: Distributed verification of rare properties using importance splitting observers. ECEASST (2015)
  31. Kahn, H., Marshall, A.W.: Methods of reducing sample size in Monte Carlo computations. Oper. Res. 1(5), 263–278 (1953)
  32. Larsen Kim, Behrmann Gerd, Brinksma Ed, Fehnker Ansgar, Hune Thomas, Pettersson Paul, Romijn Judi, As Cheap as Possible: Effcient Cost-Optimal Reachability for Priced Timed Automata, Computer Aided Verification (2001) ISBN:9783540423454 p.493-505, 10.1007/3-540-44585-4_47
  33. Larsen Kim G., Pettersson Paul, Yi Wang, Uppaal in a nutshell, 10.1007/s100090050010
  34. Larsen Kim G., Skou Arne, Bisimulation through probabilistic testing, 10.1016/0890-5401(91)90030-6
  35. Larsen K.G., Larsson F., Pettersson P., Yi W., Efficient verification of real-time systems: compact data structure and state-space reduction, 10.1109/real.1997.641265
  36. Okamoto Masashi, Some inequalities relating to the partial sum of binomial probabilities, 10.1007/bf02883985
  37. Sen Koushik, Viswanathan Mahesh, Agha Gul, Statistical Model Checking of Black-Box Probabilistic Systems, Computer Aided Verification (2004) ISBN:9783540223429 p.202-215, 10.1007/978-3-540-27813-9_16
  38. Sen Koushik, Viswanathan Mahesh, Agha Gul, On Statistical Model Checking of Stochastic Systems, Computer Aided Verification (2005) ISBN:9783540272311 p.266-280, 10.1007/11513988_26
  39. Sen K., Viswanathan M., Agha G., VESTA: A statistical model-checker and analyzer for probabilistic systems, 10.1109/qest.2005.42
  40. Wald A., Sequential Tests of Statistical Hypotheses, 10.1214/aoms/1177731118
  41. Wognsen Erik Ramsgaard, Haverkort Boudewijn R., Jongerden Marijn, Hansen René Rydhof, Larsen Kim Guldstrand, A Score Function for Optimizing the Cycle-Life of Battery-Powered Embedded Systems, Lecture Notes in Computer Science (2015) ISBN:9783319229744 p.305-320, 10.1007/978-3-319-22975-1_20
  42. Yi Wang, Pettersson Paul, Daniels Mats, Automatic Verification of Real-Time Communicating Systems by Constraint-Solving, Formal Description Techniques VII (1995) ISBN:9781504128810 p.243-258, 10.1007/978-0-387-34878-0_18
  43. Younes, H.L.S.: Verification and Planning for Stochastic Processes with Asynchronous Events. Ph.D. thesis, Carnegie Mellon (2005)
  44. Zuliani Paolo, Platzer André, Clarke Edmund M., Bayesian statistical model checking with application to Stateflow/Simulink verification, 10.1007/s10703-013-0195-3
Bibliographic reference Larsen Kim, Guldstrand ; Legay, Axel. On the Power of Statistical Model Checking.7th International Symposium, ISoLA 2016 (10/10/2016). In: Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications Lecture Notes in Computer Science, Springer International Publishing : Cham2016
Permanent URL https://hdl.handle.net/2078.1/210475