École Nationale Supérieure de
Techniques Avancées

Résumé

Dans le cadre de la vérification de systèmes hybrides, les approximations induites par les calculs et les incertitudes sur les paramètres et conditions initiales d’un système peuvent être traitées par des calculs utilisant des intervalles. Depuis sa découverte, la méthode de déduction automatique dite des tableaux a été étendue avec diverses théories axiomatiques, mais aucune de ces extensions ne permet à ce jour la prise en charge d’intervalles de flottants. La présente étude vise ainsi à explorer dans quelle mesure la méthode des tableaux pourrait être étendue avec une théorie axiomatique des intervalles, en vue d’en tirer parti pour la vérification de systèmes hybrides. Pour ce faire, un prouveur implémentant la méthode des tableaux pour la logique classique du premier ordre a d’abord été conçu. Les propriétés à exprimer sur nos intervalles de flottants ont été précisées, et de nouvelles règles d’inférences ont été conçues, puis implémentées sur le prouveur initial. L’outil ainsi développé permet d’obtenir la preuve de formules de la logique du premier ordre (agrémentée de l’égalité et de la relation d’ordre usuelle sur les réels) faisant intervenir les propriétés d’inclusion et d’appartenance à un intervalle fermé borné.