UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata

Petr Bulychev, Alexandre David, Kim Guldstrand Larsen, Marius Mikučionis, Danny Bøgsted Poulsen, Axel Legay, Zheng Wang

Publikation: Bidrag til tidsskriftKonferenceartikel i tidsskriftForskningpeer review

74 Citationer (Scopus)


This paper offers a survey of U PPAAL - SMC, a major extension of the real-time verification tool
U PPAAL. U PPAAL - SMC allows for the efficient analysis of performance properties of networks of
priced timed automata under a natural stochastic semantics. In particular, U PPAAL - SMC relies on
a series of extensions of the statistical model checking approach generalized to handle real-time
systems and estimate undecidable problems. U PPAAL - SMC 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
TidsskriftElectronic Proceedings in Theoretical Computer Science
Sider (fra-til)1-16
Antal sider17
StatusUdgivet - 2012
Begivenhed10th Workshop on Quantitative Aspects of Programming Languages and Systems - Tallinn, Estland
Varighed: 31 mar. 20121 apr. 2012
Konferencens nummer: 10th


Konference10th Workshop on Quantitative Aspects of Programming Languages and Systems

Fingeraftryk Dyk ned i forskningsemnerne om 'UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata'. Sammen danner de et unikt fingeraftryk.