VeSTA (Verification of Simulations for Timed Automata)

Organisation:	Laboratoire d'Informatique de l'Université de Franche-Comté - LIFC (Besançon, FRANCE)
Functionality:	Verification of Real-Time Systems
Tools used:	CADP (Construction and Analysis of Distributed Processes) KRONOS-OPEN
Period:	2006
Description:	Component-based modelling of timed systems consists of decomposing the system into smaller components, which are modelled as timed automata. The model of the entire system is obtained by putting together the individual components using an appropriate parallel composition operator "||". Then, two kinds of properties can be checked on this model: global properties, which involve all the components in the system, and local properties, which concern only individual components or assemblings of components. Global properties can be checked on the whole model, with the risk of state space explosion. As regards local properties, a promising alternative is to check them only on the components or assemblings of components they refer to, in order to keep the size of the models small. Obviously, this works only if the properties checked locally on components are preserved by parallel composition, such that they still hold on the entire model. The parallel composition operator used preserves safety properties, but not liveness and bounded-response properties. The divergence-sensitive and stability-respecting tau-simulation relation on timed automata defined by the authors preserves all linear properties expressed in MITL (Metric Interval Temporal Logic). It can therefore be used to ensure preservation of MITL properties by parallel composition: if the timed automaton "C||Env" denoting the composition of C with an environment Env is simulated by the timed automaton denoting C, then all linear properties established on C are preserved when C is integrated in its environment. This tau-simulation relation is defined as follows: (1) if "C||Env" can do an action of C after some amount of time, then C could do the same action after the same amount of time, and (2) internal actions of Env must stutter. Divergence-sensitivity ensures that internal actions of Env will not take control forever, and stability respect guarantees that the integration of C in Env will not create new deadlocks. VeSTA (Verification of Simulations for Timed Automata) is a push-button tool that automates the verification of this tau-simulation in the framework of component-based timed systems. VeSTA allows to check the correct integration of a component in its environment, meaning that local properties of the component are preserved when it is merged into its environment. The architecture of VeSTA was inspired by that of KRONOS-OPEN and the tool is connected to the OPEN/CAESAR verification environment of CADP. A component-based timed system is defined in VeSTA as a set of components modelled as timed automata, possibly having attached their local properties to be preserved, the types of the variables used in the components, and the interactions between components. Assemblings of components, called composites, created by parallel composition of individual components, are generated automatically in the form of ".exp" files. All these elements can be specified using the graphical user interface of the tool. VeSTA consists of three modules: translator, simul, and profounder. Starting from a component system, translator produces a C program implementing the successor function of the symbolic graph corresponding to each composite involved in the simulation. This program respects the OPEN/CAESAR interface and thus can be used in conjunction with all the on-the-fly verification tools provided by CADP. The simul and profounder modules (the latter being imported from KRONOS-OPEN) allow to check the stability-respecting tau-simulation and the divergence-sensitive condition, respectively. VeSTA was applied on a number of case-studies, among which a CSMA-CD protocol and a production cell. Significant performance gains (up to an order of magnitude) were observed when checking properties and tau-simulation locally on components w.r.t. checking properties globally on the entire system.
Conclusions:	The approach using tau-simulations shown to be an effective solution for checking local properties of individual components during the incremental modelling of component-based timed systems. Future work includes the study of other parallel composition operators and their adequacy with the tau-simulation proposed, and also the investigation of the applicability of the approach to parametric systems.
Publications:	[Bellegarde-Julliand-Mountassir-Oudot-06] Françoise Bellegarde, Jacques Julliand, Hassan Mountassir, and Emilie Oudot. "The tool VeSTA: Verification of Simulations for Timed Automata". Technical Report RT2006-01, LIFC, Besançon, France, July 2006. Available on-line at: http://lifc.univ-fcomte.fr/publis/papers/pub/2006/RT2006-01.pdf or from the CADP Web site in PDF or PostScript [Oudot-06] Emilie Oudot. "Contributions à la vérification incrémentale des systèmes temporisés à composants". PhD thesis, Université de Franche-Comté (France), December 2006. Available on-line at: http://lifc.univ-fcomte.fr/publis/manuscrits/theseOudot06.pdf or from the CADP Web site in PDF or PostScript
Contact:	Emilie Oudot Laboratoire d'Informatique de l'Université de Franche-Comté (LIFC) 16, route de Gray F-25030 Besançon Cedex France Tel: +33 (0)3 81 66 66 51 Fax: +33 (0)3 81 66 64 50 E-mail: Emilie.Oudot@lifc.univ-fcomte.fr
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page