Abstract:
Nous considerons le probleme de la verification automatique de
proprietes de systemes reactifs. En effet, leur caractere parallele,
non-deterministe et eventuellement reparti conduit a des fautes de
conception frequentes et a une mise au point plus difficile. Le
developpement de programmes prouves par rapport a une specification
peut apparaitre comme une solution a ce double probleme. Dans ce
cadre, nous decrivons la realisation d'un environnement fonde sur le
formalisme UNITY. Pour realiser les preuves necessaires, celui-ci
utilise un demonstrateur de theoremes et un calculateur de formules
Presburger. A partir de quelques exemples significatifs, nous
exposons les principales difficultes rencontrees.
Michel Charpentier <
>
Last modified: Thu Feb 10 13:36:55 EST 2000