Date: Mon, 9 Sep 1996 13:20:34 +0200 To: concurrency@cwi.nl Subject: ANNOUNCE: XEVE (v1), a Verification Environment for Esterel From: Amar Bouali Content-Type: text Content-Length: 1680 Dear all, We are glad to announce availability of the verification environment XEVE for Esterel. Esterel is a language to program synchronous reactive systems. It has a clean mathematical semantics in terms of (Mealy) Finite State Machines (FSMs). The main characteristics of Esterel are: - modular imperative programming style; - synchronous parallelism of processes; - communication by signal broadcasting (no rendez-vous mechanism); - instantaneous reaction of processes to input events. FSMs are generated either explicitly (enumerated states) or implicitly as boolean circuits. (See URL http://cma.cma.fr/Esterel/ for more details on the language, its compiler and on how to get it). The verification environment is made of a set of UNIX processors implementing verification functions over the FSM representation. The most striking features of these tools are: - Reachable state space construction and analysis - FSM minimisation with respect to a symbolic bisimulation equivalence, modulo a set of hidden signals (introducing non-determinism). - Checking of Safety properties (as well as restriscted subclass of liveness properties) embodied into Esterel observers put in parallel with the program to verify. - Source recovery of verification diagnostics from previous verification functions, graphically simulated using the XES simulator panel for Esterel. Current distribution is available for Sun4OS4, Solaris, PC-Linux and DEC-Alpha architectures. All information can be obtained from: http://cma.cma.fr/Verification/Esterel/ or by emailing to: fc2team@cma.cma.fr Enjoy, Amar Bouali, Annie Ressouche, Valerie Roy, Robert de Simone.