Welcome to the Esterel Verification
Environment
A new version of Xeve is
now available. Xeve now takes part the Esterel v5_91
compiler distribution tape. Xeve version number is now set
to the Esterel compiler version number. Still, Xeve v5_91
can be downloaded separately. Download
it now ! Check the changes
between the version v5_91 and the previous versions.
What is Xeve ?
Xeve is a graphical interface environment for the
(symbolic) analysis and verification of Esterel programs
modeled as Finite State Machines (FSM). It is developed
jointly by INRIA and Ecole des Mines/CMA as part of the TICK
research project (coming from the MEIJE project)
Its main features are:
- FSM model construction from netlist descriptions of Esterel
programs
- FSM minimisation using a notion of bisimulation
equivalence
- output signal status checking under input constraints.
- verification of safety properties expressed by observers
by means of output signal status checking.
- input sequences production in case of verification failure.
Some pictures
of Xeve.
Around Xeve
Tools that are connected to Xeve as front-ends or back-ends, or as
complementary tools:
- fc2symbmin
a Finite State Mealy Machine analyzer. It works on FSMs generated
by the Esterel compiler and described in the Fc2
format. Analysis functions comprise FSM minimization with
a symbolic treatment of transition labels and modulo
signal hiding, FSM synchronous product, and FSM equivalence
checking.
- Atg
a graphical editor for automata, used by Xeve to graphically
visualize the minimized FSMs.
- Xes the Esterel graphical
simulator used to play on the source the execution sequences
extracted from model-checking diagnostics. Xes is
distributed together with the Esterel compiler.
WWW pages related to Xeve:
For any request, remark, experience, send email to esterel-team@sophia.inria.fr
Bugs, usage problems should be reported to esterel-bugs@sophia.inria.fr
Enjoy,
Amar.Bouali@sophia.inria.fr