The tool VeSTA

1. General Presentation

VeSTA (Verification of Simulation for Timed Automata) is a push-button tool allowing to check the correct integration of a component in an environment, for component-based timed models. Each component is modeled as a timed automaton, and the interactions between the components are given in terms of actions which synchronize. By correct integration, we mean that the local properties of the component are preserved when this component is merged into an environment. This correctness is checked by means of a so-called divergence-sensitive and stability-respecting timed tau-simulation , which guarantees the preservation of all timed linear properties expressed in the logic MITL (Metric Interval Timed Logic).

Note also that the way VeSTA was created allows to connect the models considered in the tool to the verification platform Open-Caesar. This was inspired by the Open-Kronos tool.

2. Overview

VeSTA considers component-based timed models consisting of a set of components, modeled as timed automata, which interact by synchronizing on common actions. The screenshot below shows a part of the Graphical User Interface of VeSTA. In particular, it shows the Interactions tab representing the timed model currently considered. The model is displayed as a graph, where each node represents a component, and lines between nodes models the interactions between components.



The different features of the tool are the following :

• Creating the timed model, i.e., the components and their interactions,
• Integrating components in their environment (this creates what we call composite components in VeSTA),
• Checking that these integrations are correct, by verifying a simulation relation between components, and thus, concluding if the local properties of the components are preserved when they are merged into their environment. A graphical diagnostic is provided if the simulation is not checked succesfully.

As optional feature, VeSTA offers the possibility to specify, for the components, their local properties which must be preserved. This will allow to optimize the verification of the simulation, but, in return, only ensure preservation for the specified properties.

There are three back-ends, written in C, in the tool: translator, simul and profounder:

• translator in an executable taking as input the two components for which the simulation must be checked. It creates a file .c, implementing date structures and functions to generate a symbolic graph (the so-called simulation graph) for each input component. This file .c can be connected to the Open-Caesar platform.
• simul is the executable which checks the stability-respecting timed tau-simulation. The file is created each time a new simulation is checked.
• profounder is the executable which checks the divergence-sensitive part of the simulation. As simul, it is also created each time divergence-sensitivity has to be verified. Note that profounder was implemented by Stavros Tripakis. More information about this module are available on the Open-Kronos web page.

3. Download

VeSTA is available for Linux systems. The GUI is written for Java VM 1.5 (if needed, see http://java.sun.com to download the Java Runtime Environment). To create the back-ends simul and profounder, you will need the gcc compiler. The tool was for the moment only tested with gcc 3.3.2.
You also need CADP to be installed to run VeSTA.

To get VeSTA, download the following file:
VeSTA.tar.gz
Uncompress the archive and see the documentation to get informations about how to install and run the tool.