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: http://www.cmi.univ-mrs.fr/~niebert/docs/else.pdf or from the CADP Web site in PDF or PostScript
Contact:	Peter Niebert LIF, Université de Provence 39, rue Jolliot-Curie F-13453 Marseille Cedex 13 FRANCE Tel: +33 (0)4 91 11 36 24 Fax: +33 (0)4 91 11 36 02 E-mail: [email protected]
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