UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata

Abstract

This paper offers a survey of uppaalsmc, a major extension of the real-time verification tool uppaal. uppaalsmc allows for the efficient analysis of performance properties of networks of priced timed automata under a natural stochastic semantics. In particular, uppaalsmc relies on a series of extensions of the statistical model checking approach generalized to handle real-time systems and estimate undecidable problems. uppaalsmc comes together with a friendly user interface that allows a user to specify complex problems in an efficient manner as well as to get feedback in the form of probability distributions and compare probabilities to analyze performance aspects of systems. The focus of the survey is on the evolution of the tool - including modeling and specification formalisms as well as techniques applied - together with applications of the tool to case studies.

In Proceedings QAPL 2012, arXiv:1207.0559

References in corpus (4)

• On Zone-Based Analysis of Duration Probabilistic Automata
• Computing Nash Equilibrium in Wireless Ad Hoc Networks: A Simulation-Based Approach
• Distributed Parametric and Statistical Model Checking
• Proceedings 10th International Workshop on Parallel and Distributed Methods in verifiCation

Cited by in corpus (14)

• PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games
• Applying Formal Methods to Networking: Theory, Techniques and Applications
• Statistical Model Checking for Biological Applications
• The Probabilistic Model Checker Storm (Extended Abstract)
• Modelling, Verification, and Comparative Performance Analysis of the B.A.T.M.A.N. Protocol
• Formally Modeling Autonomous Vehicles in LNT for Simulation and Testing
• Early Validation of Cyber-Physical Space Systems via Multi-Concerns Integration
• Simulation-based Safety Assessment of High-level Reliability Models
• Analysing oscillatory trends of discrete-state stochastic processes through HASL statistical model checking
• Probabilistic Analysis of Weakly-Hard Real-Time Systems
• Faster Statistical Model Checking for Unbounded Temporal Properties
• Formal Verification of a Programmable Hypersurface
• Verification of Markov Decision Processes using Learning Algorithms
• Quantitative Aspects of Programming Languages and Systems over the past $2^4$ years and beyond