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.
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