Uppaal is an integrated tool environment for modeling, simulation, formal verification, performance analysis, and synthesis of real-time systems. It targets cyber physical 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 application areas include real-time controllers and communication protocols in particular, those where timing aspects are critical.
With more than 15 years of history of being a leading verification tool for real-time- and cyber-physical-systems, the development of the Uppaal tool-suite continues. We are proud to announce a new major release that contains several new ground-breaking features.
Uppaal 5.0 now supports modelling of stochastic- and hybrid-systems (combining discrete state and continous variables) offering tool support for performance analysis, optimization, and controller synthesis using machine learning.
All the features of modelling timed automata, symbolic model-checker, and simulation/animation well-known from Uppaal4 are also available in the new release. Several improvements to the user-interface, verification engine, documentation and its APIs are included.
Uppaal 5.0 comes with a brand new additional analysis engine that through precise simulations targets scalable performance analysis of system models that, in addition to time constraints, may contain probabilistic information on states and transitions to model a variety of resource usages. Further, the evolution of dynamic variables may be described though ordinary differential equations. Further, linking the model with external C-code greatly improves speed and flexibility. Combining this information with a sophisticated analysis technique known as statistical model-checking, Uppaal 5.0 enables the developer to formulate probabilistic queries to gain deep insights into the stochastic behavior of the model, and hence performance of the modelled systems, e.g. speed, ressource- or energy-consumption.
Uppaal 5.0 comes with a powerful plot composer that allows the results of queries to be visualized in a multitude of digestible ways, such as probability distributions, histograms, and function plots of how the variables in a model evolves. This allows query results to be compared visually side by side, and allows for making nice plots for documentation.
Often an engineer is tasked to find the best safe way to control a system or solve an optimization problem. Uppaal 5.0 offers a novel component (Uppaal-Stratego) that offers automated synthesis of a control strategy, that may be used directly or indirectly in a product, i.e. a case of model-predictive control. The engineer describes the system and environment to be controlled as a game of controllable and uncontrollable actions. Uppaal-Stratego then attempts to compute a winning strategy for the controller that brings the environment into the desired "winning" configuration.
Using machine learning based techniques, the performance of the controller can be optimized with respect to a user defined metric. The controller requirements may contain safety constraints as well as optimizations like cost minization or gain maximization.
In the initial stages of systems design and design exploration, it often happens that the modelled system is able to reach certain (typically undesirable) states ("bugs"). Uppaal 5 comes with a new randomized simulation engine that is equipped with an accelerated search mode that often is orders of magnitude faster than symbolic analysis for falsification of such properties. This speeds up the initial engineering stages and saves the time consuming and computational heavy formal verification for more mature designs.
In addition to the existing symbolic simulator, Uppaal 5.0 comes with a new concrete state simulator and animator that allows the user to explore the system model by choosing not only which transition to take next, but exactly when. This gives an intuitive and very fine-grained interactive simulation interface. It also facilitates manual “playing” and exploration of a synthesized control strategy.
Uppaal primarily aims at analyzing system models. However, Uppaal 5.0 also features a potent test sequence generator. Using the model-checking analysis engine, Uppaal is capable of computing an execution sequence of the model that leads to an interesting system state. Under certain assumptions (determinism), such a sequence can be used as a test case. The use annotates the model with test code fragments in states and transitions that are emitted to a test case file in the sequence dictated by the computed sequence. Uppaal 5.0 supports a user-controllable combination of generating targeted test cases and achieving structural coverage of the model. The Test Cases feature is enabled in the Tools menu.
In addition to the main features listed above, Uppaal5 brings an improved editor, and its graphical user interface contains a multitude of general improvements that enhance the user experience and provides a uniform look&feel across the supported platforms.
These are elaborated on Uppaal5 web pageIf you are interested in purchasing a licence, evaluating the tool-suite, or request further information, please send an email to sales@veriaal.dk