Syntax-Driven Reachable State Space Construction of Synchronous Reactive Programs

We consider in the current paper the issue of exploiting the structural form of Esterel programs [BG92] to partition the algorithmic RSS (reachable state space) fix-point construction used in modelchecking techniques [CGP99]. The basic idea sounds utterly simple, as seen on the case of sequential composition: in P; Q, first compute entirely the states reached in P, and then only carry on to Q, each time using only the relevant local transition relation part. Here a brute-force symbolic breadth-first search would have mixed the exploration of P

• Type: Conference
• Year: 2005
• Where: CAV
• Authors: Eric Vecchié, Robert de Simone
• Keywords: CAV 2005, Formal Methods, Reachable State Space, Symbolic Breadth-first Search, Transition Relation Part