This tutorial paper surveys the main features of Uppaal SMC, a model checking approach in Uppaal family that allows us to reason on networks of complex real-timed systems with a stochastic semantic. We demon- strate the modeling features of the tool, new verification algorithms and ways of applying them to potentially complex case studies.
Alur Rajeev, Feder Tomás, Henzinger Thomas A., The benefits of relaxing punctuality, 10.1145/227595.227602
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
Behrmann Gerd, David Alexandre, Larsen Kim G., A Tutorial on Uppaal, Lecture Notes in Computer Science (2004) ISBN:9783540230687 p.200-236, 10.1007/978-3-540-30080-9_7
Behrmann Gerd, David Alexandre, Larsen Kim Guldstrand, Pettersson Paul, Yi Wang, Developing UPPAAL over 15 years, 10.1002/spe.1006
Bulychev, P., David, A., Larsen, K.G., Legay, A., Li, G., Poulsen, D.B.: Rewrite-based statistical model checking of wmtl. In: Runtime Verification, vol. 7687 of LNCS, pp. 260–275 (2012)
Bulychev Peter, David Alexandre, Guldstrand Larsen Kim, Legay Axel, Li Guangyuan, Bøgsted Poulsen Danny, Stainer Amelie, Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic, Logic for Programming, Artificial Intelligence, and Reasoning (2012) ISBN:9783642287169 p.168-182, 10.1007/978-3-642-28717-6_15
Bulychev Peter, David Alexandre, Guldstrand Larsen Kim, Legay Axel, Mikučionis Marius, Bøgsted Poulsen Danny, Checking and Distributing Statistical Model Checking, Lecture Notes in Computer Science (2012) ISBN:9783642288906 p.449-463, 10.1007/978-3-642-28891-3_39
Behrmann, G., David, A., Larsen, K.G., Yi, W.: Unification & sharing in timed automata verification. In: SPIN Workshop 03, vol. 2648 of LNCS, pp. 225–229 (2003)
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
Behrmann Gerd, Fehnker Ansgar, Hune Thomas S., Larsen Kim G., Pettersson Paul, Romijn Judi, Vaandrager Frits W., Minimum-Cost Reachability for Priced Timed Automata, 10.7146/brics.v8i3.20457
Behrmann, G., Hune, T., Vaandrager, F.: Distributed timed model checking: How the search order matters. In: Proceedings of 12th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, Chicago, Springer, Jul (2000)
Broy, M., Jonsson, B., Katoen, J-P., Leucker, M., Pretschner, A. (eds.): Model-based testing of reactive systems, advanced lectures the volume is the outcome of a research seminar that was held in Schloss Dagstuhl in January 2004, vol. 3472 of Lecture Notes in Computer Science. Springer (2005)
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
Clarke Edmund M., Faeder James R., Langmead Christopher J., Harris Leonard A., Jha Sumit Kumar, Legay Axel, Statistical Model Checking in BioLab: Applications to the Automated Analysis of T-Cell Receptor Signaling Pathway, Computational Methods in Systems Biology (2008) ISBN:9783540885610 p.231-250, 10.1007/978-3-540-88562-7_18
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Chernoff Herman, A Measure of Asymptotic Efficiency for Tests of a Hypothesis Based on the sum of Observations, 10.1214/aoms/1177729330
CLOPPER C. J., PEARSON E. S., THE USE OF CONFIDENCE OR FIDUCIAL LIMITS ILLUSTRATED IN THE CASE OF THE BINOMIAL, 10.1093/biomet/26.4.404
David Alexandre, Du Dehui, Larsen Kim G., Legay Axel, Mikučionis Marius, Poulsen Danny Bøgsted, Sedwards Sean, Statistical Model Checking for Stochastic Hybrid Systems, 10.4204/eptcs.92.9
David Alexandre, Du Dehui, Guldstrand Larsen Kim, Legay Axel, Mikučionis Marius, Optimizing Control Strategy Using Statistical Model Checking, Lecture Notes in Computer Science (2013) ISBN:9783642380877 p.352-367, 10.1007/978-3-642-38088-4_24
David, A., Jensen, P.G., Larsen, K.G., Legay, A., Lime, D., Søresensen, M.G., Taankvist, J.H.: On time with miniam expected cost
David Alexandre, Larsen Kim G., Legay Axel, Mikučionis Marius, Poulsen Danny Bøgsted, van Vliet Jonas, Wang Zheng, Statistical Model Checking for Networks of Priced Timed Automata, Lecture Notes in Computer Science (2011) ISBN:9783642243097 p.80-96, 10.1007/978-3-642-24310-3_7
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
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
Henriques David, Martins Joao G., Zuliani Paolo, Platzer Andre, Clarke Edmund M., Statistical Model Checking for Markov Decision Processes, 10.1109/qest.2012.19
Hartmanns, A.: Model-checking and simulation for stochastic timed systems. In: Bernhard, K.A., De Boer, F.S., Marcello M.B. (eds.) FMCO, vol. 6957 of Lecture Notes in Computer Science, pp. 372–391. Springer (2010)
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
Jha Sumit K., Clarke Edmund M., Langmead Christopher J., Legay Axel, Platzer André, Zuliani Paolo, A Bayesian Approach to Model Checking Biological Systems, Computational Methods in Systems Biology (2009) ISBN:9783642038440 p.218-234, 10.1007/978-3-642-03845-7_15
Kwiatkowska M., Norman G., Parker D., PRISM 2.0: a tool for probabilistic model checking, 10.1109/qest.2004.1348048
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
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
Larsen Kim G., Pettersson Paul, Yi Wang, Uppaal in a nutshell, 10.1007/s100090050010
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
Theelen, B.D.: Performance modelling for system-level design. Ph.D. thesis, Eindhoven University of Technology, (2004) ISBN 90-386-1633-3
Younes, H.L.S.: Verification and planning for stochastic processes with asynchronous events. Ph.D. thesis, Carnegie Mellon (2005)
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
Bibliographic reference
Legay, Axel ; et. al. UPPAAL SMC: A tutorial. In: International Journal on Software Tools for Technology Transfer, Vol. 17, no.4, p. 20 (2015)