Uppaal-now, next and future

Abstract. Uppaal is a tool for modeling, simulation and verification of real-time systems, developed jointly by BRICS at Aalborg University and the Department of Computer Systems at Uppsala University. The tool is appropriate for systems that can be modeled as a collection of non-deterministic processes with finite control structure and real-valued clocks, communicating through channels or shared variables. Typical ap-plication areas include real-time controllers and communication proto-cols, in particular those where timing aspects are critical. This paper reports on the currently available version and summarizes de-velopments during the last two years. We report on new directions that extends Uppaal with cost-optimal exploration, parametric modeling, stop-watches, probablistic modeling, hierachical modeling, executable timed automata, and a hybrid automata animator. We also report on recent work to improve the efficiency of the tool. In particular, we out-line Clock Difference Diagrams (CDDs), new compact representations of states, a distributed version of the tool, and application of dynamic partitioning. Uppaal has been applied in a number of academic and industrial case studies. We describe a selection of the recent case studies. 1 Current Version of Uppaal In the following, we give a brief overview on Uppaal’s maturing over the years and explain the core functionalities of the current release version