UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata

TL;DR

UPPAAL-SMC is an extension of the UPPAAL tool that enables efficient statistical model checking of priced timed automata, supporting performance analysis of real-time systems with stochastic semantics.

Contribution

This paper surveys the evolution, modeling, techniques, and applications of UPPAAL-SMC, highlighting its capabilities for analyzing performance properties of timed automata.

Findings

Supports analysis of performance properties in timed automata

Provides probability distributions and comparison tools

Applied to various case studies for validation

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.