Skip to Main content Skip to Navigation

XEVE : an ESTEREL Verification Environment : (Version v1_3)

Amar Bouali 1
1 MEIJE - Concurrency, Synchronization and Real-time Programming
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : XEVE is a verification environment for ESTEREL programs modeled as Finite State Machines {FSMs) with a user-friendly graphical interface. The ESTEREL compiler translates a program into a system of boolean equations with latch that defines a FSM implicitly. XEVE works on these implicitly defined FSMs. It is based on the TiGeR library which provides efficient data structures and algorithms to manipulate FSMs symbolically using BDDs. It takes as input the set of boolean equations of a FSM described in the Blif format (Berkeley Logical Interchange Format). XEVE provides two main verification functions. The first function is the FSM state minimization using a notion of bisimulation equivalence that relates states indistinguishable when exploring the FSM graph from them. The minimization is made modulo a set of input/output signals declared as hidden. Minimized FSMs are generated explicitly in a textual format called Fc2 that can be loaded in the tool Atg for graphical exploration. The other verification function is the checking of the status of output signals: one can verify if an output is possibly emitted or not. This checking can be made modulo the fixing of input signals to some value (0 for absent or 1 for present). When an output is found possibly emitted or not, a minimal execution trace leading to a state emitting or not the signal is saved in the csimul format. The sequence can played within Xes the Esterel graphical simulator.
Document type :
Complete list of metadata
Contributor : Rapport de Recherche Inria <>
Submitted on : Friday, May 19, 2006 - 6:42:35 PM
Last modification on : Saturday, January 27, 2018 - 1:31:29 AM
Long-term archiving on: : Sunday, April 4, 2010 - 7:54:31 PM


  • HAL Id : inria-00069957, version 1



Amar Bouali. XEVE : an ESTEREL Verification Environment : (Version v1_3). [Technical Report] RT-0214, INRIA. 1997, pp.23. ⟨inria-00069957⟩



Record views


Files downloads