UPPAAL v.4™

 The verification platform

UPPAAL is an integrated tool environment for modeling, simulation and, verification of real-time embedded systems. Typical application areas of UPPAAL includes real-time controllers and communication protocols in particular, those where timing aspects are critical.

The tool environment

V.4 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. Uppaal v.4 consists of three main parts.

State of art criterias

UPPAAL v.4 has been developed specifically for the end user in mind by implementing two ideas of concept. They are efficiency and ease of usage. The model-checker has in its on-the-fly searching technique a state of art function which is crucial to the efficiency when a user is modeling, simulating or trying to verificate a result of a real-time system.

Another important key is the application of a symbolic technique that reduces verification problems to that of efficient manipulation and solving of constraints.

To facilitate modeling and debugging, the UPPAAL model-checker may automatically generate a diagnostic trace that explains why a property is (or is not) satisfied by a system description. The diagnostic traces generated by the model-checker can be loaded automatically to the simulator, which may be used for visualization and investigation of the trace.