XEVE : an ESTEREL Verification Environment : (Version v1_3) - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport Technique) Année : 1997

XEVE : an ESTEREL Verification Environment : (Version v1_3)

Résumé

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.
Fichier principal
Vignette du fichier
RT-0214.pdf (692.92 Ko) Télécharger le fichier

Dates et versions

inria-00069957 , version 1 (19-05-2006)

Identifiants

  • HAL Id : inria-00069957 , version 1

Citer

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

Partager

Gmail Facebook X LinkedIn More