UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata

This paper offers a survey of U PPAAL - SMC, a major extension of the real-time verification toolU PPAAL. U PPAAL - SMC allows for the efficient analysis of performance properties of networks ofpriced timed automata under a natural stochastic semantics. In particular, U PPAAL - SMC relies ona series of extensions of the statistical model checking approach generalized to handle real-timesystems and estimate undecidable problems. U PPAAL - SMC comes together with a friendly userinterface that allows a user to specify complex problems in an efficient manner as well as to getfeedback in the form of probability distributions and compare probabilities to analyze performanceaspects of systems. The focus of the survey is on the evolution of the tool – including modeling andspecification formalisms as well as techniques applied – together with applications of the tool to casestudies.