thesis

Specification et preuve de systemes dynamiques

Defense date:

Jan. 1, 1992

Edit

Institution:

Rennes 1

Disciplines:

Authors:

Directors:

Abstract EN:

Pas de résumé disponible.

Abstract FR:

Signal est un langage synchrone, a flots de donnees, destine a la specification de systemes reactifs et temps-reel. Cette these etudie des methodes et outils de preuve de programmes signal. Un codage polynomial, dans le corps des entiers modulo trois, decrit les aspects logiques et temporels des programmes; demontrer une propriete d'un systeme reactif consiste a verifier, au moyen d'outils de calcul formel, une propriete algebrique equivalente. La representation des fonctions polynomiales par graphes de decision ternaires permet une mise en uvre efficace de ces calculs