Laboratoire d'Informatique de l'Université de Franche-Comté - LIFC
Verification of Real-Time Systems
CADP (Construction and Analysis of Distributed Processes)
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.
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.
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
Laboratoire d'Informatique de l'Université de Franche-Comté (LIFC)
16, route de Gray
F-25030 Besançon Cedex
Tel: +33 (0)3 81 66 66 51
Fax: +33 (0)3 81 66 64 50
|Further remarks:||This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software|