Syntax-driven optimisations for reachable state space construction of ESTEREL programs
by Eric Vecchie, Robert de Simone
International Journal of Embedded Systems (IJES), Vol. 2, No. 3/4, 2006

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.

Online publication date: Sun, 12-Aug-2007

The full text of this article is only available to individual subscribers or to users at subscribing institutions.

 
Existing subscribers:
Go to Inderscience Online Journals to access the Full Text of this article.

Pay per view:
If you are not a subscriber and you just want to read the full contents of this article, buy online access here.

Complimentary Subscribers, Editors or Members of the Editorial Board of the International Journal of Embedded Systems (IJES):
Login with your Inderscience username and password:

Username:        Password:          Forgotten your password?

Want to subscribe?
A subscription gives you complete access to all articles in the current issue, as well as to all articles in the previous three years (where applicable). See our Orders page to subscribe.

If you still need assistance, please email subs@inderscience.com