Database of Research Tools Developed Using CADP

Verification of Real-Time Systems using ELSE and CADP

Organisation: LIF, Université de Provence (Marseille, FRANCE)

Functionality: Symbolic state space generation and analysis of timed automata

Tools used: ELSE (symbolic state space generator for timed automata)
CADP (Construction and Analysis of Distributed Processes)

Period: 2003

Description: ELSE is a prototype state space generator for timed automata, which compiles timed automata to C programs that link with CADP. ELSE uses clock constraints to abstract the state space to a finite set of equivalence classes, and partial order reduction techniques to avoid the generation of irrelevant interleavings.

ELSE differentiates from classical tools such as Kronos and Uppaal in using so-called event zones to represent time constraints. ELSE includes a library for event zones, called elsezone.

Conclusions: The ELSE prototype has been experimented on academic examples, which tend to show that the event zone approach is more efficient than classical approaches. On some example series, exponential savings have been observed.

Publications: [Zennou-Yguel-Niebert-03] Sarah Zennou, Manuel Yguel, and Peter Niebert. "ELSE: A New Symbolic State Generator for Timed Automata". In Proceedings of the 1st International Workshop on Formal Modeling and Analysis of Timed Systems FORMATS'2003 (Marseille, France), September 2003.
Available on-line at:
or from the CADP Web site in PDF or PostScript
Peter Niebert
LIF, Université de Provence
39, rue Jolliot-Curie
F-13453 Marseille Cedex 13
Tel: +33 (0)4 91 11 36 24
Fax: +33 (0)4 91 11 36 02

Further remarks: This tool, amongst others, is described on the CADP Web site:

Last modified: Thu Feb 11 12:23:12 2021.

Back to the CADP research tools page