Title: Syntax-driven optimisations for reachable state space construction of ESTEREL programs

Authors: Eric Vecchie, Robert de Simone

Addresses: INRIA Sophia-Antipolis, France. ' INRIA Sophia-Antipolis, France

Abstract: We consider the issue of exploiting the structural form of ESTEREL programs (Berry and Gonthier, 1992) to partition the algorithmic Reachable State Space construction used in model-checking techniques (Clarke et al., 1999). The basic idea sounds utterly simple: in P; Q, first compute entirely the states reached in P and then carry on to Q, each time using only the relevant transition relation part. Difficulties appear in presence of parallelism: program blocks can be synchronised in various ways, which may lead to an excessive complexity in decomposition. We use the structural division as obtained from the programs syntax, some of the key |cofactoring| features of the TiGeR BDD library (Coudert et al., 1993) and heuristic orderings between internal signals.

Keywords: reactive systems; synchronous; ESTEREL; model checking; BDD; partitioning; reachable state space; cofactors; embedded systems; syntax driven optimisation.

DOI: 10.1504/IJES.2006.014858

International Journal of Embedded Systems, 2006 Vol.2 No.3/4, pp.228 - 238

Published online: 12 Aug 2007 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article