  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.
