Footnotes

Footnotes

 (1)

The architecture of the tool allows to replace an abstract domain for some datatype by another one; for instance, polyhedra could be replaved by octagons. It is also possible to add a new datatype, provided that an abstract domain for it is available (and implemented !).

 (2)

The classical method for verifying such systems is (was) to enumerate all possible valuations of Boolean variables, and to attach a numerical invariant (e.g., a polyhedra) to each of these valuations. However this method is strongly limited by the number of Boolean variables, which can be several dozens even for small LUSTRE programs. Our notion of control structure induces this method as a particular case.

 (3)

Our control structure are quite similar to the ones otaine by predicate abstraction; they are slightly more general and '`surtout" are used to solve fixpoint equations on an infinite domain, instead of being explored as a finite graph. So the result is "this subset of states in this location may be reachable" instead of "no state, or all states in this location may be reachable".

Footnotes