XEVE, an ESTEREL verification environment

Abstract

We describe the verification methods and tools we are currently developing around the language ESTEREL. This language is dedicated for the development of synchronous reactive systems such as hardware or software controllers for which the control handling aspects are predominant. The language has a strong mathematical semantics in terms of Finite State Machines. Automatic verification is then possible on this model in which we represent exhaustively all the possible behaviors of a system. Our methods are based on model minimization coupled with un-relevant behaviors masking and model checking techniques to verify correctness properties like safety and liveness ones by means of synchronous observers.