B. Dutertre. Spécification et preuve de systèmes dynamiques. Thèse de l'Université de Rennes I, IFSIC, Décembre 1992.
SIGNAL est un langage synchrone, à flots de données, destiné à la spécification de systèmes réactifs et temps-réel. Certains domaines d'application envisagés exigent une grande fiabilité et une grande sûreté de fonctionnement. Pour répondre à ces exigences, il est nécessaire de pouvoir prouver des propriétés critiques des programmes. Cette thèse a pour objet l'étude de méthodes et d'outils de validation et de preuve des systèmes réactifs décrits en SIGNAL. La vérification de propriétés repose sur une représentation équationnelle de la synchronisation et de la logique des programmes, sous la forme de systèmes dynamiques dans le corps des entiers modulo trois. L'approche retenue consiste à traduire les propriétés des systèmes réactifs en propriétés algébriques équivalentes qui peuvent être vérifiées par des outils de calcul formel. Cette approche permet notamment la vérification de propriétés exprimées soit par des formules de logique temporelle soit par d'autres systèmes dynamiques. Nous montrons comment les graphes de décision binaires utilisés dans le cadre des algèbres booléennes peuvent être étendus aux fonctions polynômiales sur un corps finis et comment cette représentation permet une mise en oeuvre performante des calculs algébriques
@PhdThesis{dutertre92a,
Author = {Dutertre, B.},
Title = {Spécification et preuve de systèmes dynamiques},
School = {Université de Rennes I, IFSIC},
Month = {December},
Year = {1992}
}
Charger la référence EndNote (.ref)
This page is part the Espresso project web site.
It has been automatically generated using the bib2html program.