PV5 ⊧ UPPAALan IDE for modelling, validating and verifying networks of timed automata

Tool set for modeling, validation and verification of real-time systems that are modelled as networks of timed automata, extended with data types.

Application domain/field

• Real-time systems
• Timed automata
• Model checking
• Simulation
• Statistical model checking

Type of tool

Framework for modeling, validating and verifying real-time systems

Internals

Some features of UPPAAL include:

• Graphical system editor
• Graphical simulator
• Requirement specification editor
• Model-checker for safety and liveness properties
• Generation of diagnostic traces in case verification fails