Les automates finis sont utilisés
pour modéliser des systèmes réactifs et peuvent
être associés à des techniques de preuves
automatiques. Cependant si la modélisation fait intervenir la
notion de temps, il n'est pas possible de rester dans le cadre des
automates finis. Les automates temporisés sont un formalisme
permettant de prendre en compte à la fois les évolutions
discrètes d'un système et les
contraintes continues de temps.
L'objectif du stage est d'étudier l'automatisation des
preuves de propriétés d'automates temporisés avec
paramètres dans le cas particulier où les contraintes
sont des formules arithmétiques simples. Pour cela on utilise la
procédure de Revesz[3] : cet algorithme engendre une formule
logique équivalente à la définition de la relation
de transition sur les états en utilisant des transformations de
graphes.
Il s'agira de réaliser un programme Caml qui à partir
de la description de l'automate calcule la formule décrivant
l'invariant. Puis on construira automatiquement dans l'assistant de
preuve Coq [1]
une preuve du fait que la formule est effectivement un invariant. Le
développement s'appuiera sur un exemple de preuve
développée dans le système Gap utilisant des
techniques analogues et sur les outils de la plateforme Calife pour la
spécification et validation de systèmes
modélisés par des automates temporisés.