ViTAL is a tool which provides model-checking of EAST-ADL systems with regard to timing/behavioral requirements.

We implement an automatic model transformation so that UPPAAL PORT can handle EAST-ADL models as input and provide functional and timing behavior of functional blocks using timed automata semantics. UPPAAL PORT is an extension of UPPAAL tool which supports simulation and model-checking without conversion or flattening to the model of network of timed automata that is usually used in UPPAAL.

UPPAAL PORT uses a Partial Order Reduction Technique (PORT) in order to improve the efficiency of the model-checking analysis.


The latest version 0.32 is available for download, see also the release notes.

Windows(v 0.32)


Screenshot of VITAL.

A Verification Tool for EAST-ADL Models using UPPAAL PORT