Date : 1996
Editeur / Publisher : [Lieu de publication inconnu] : [Éditeur inconnu] , 1996
Format : 1 vol. (125 P.)
Type : Livre / Book
Type : Thèse / ThesisLangue / Language : français / French
Résumé / Abstract : Nous presentons dans cette these la verification temporelle de programmes ecrits en langage reactif asynchrone electre, basee sur la modelisation de programmes electre par des automates hybrides, et sur l'expression en logique temporelle des proprietes a verifier. Nous montrons que les automates hybrides obtenus a partir de programmes electre possedent la qualite d'etre fortement non-zenon ; que les proprietes temporelles portant sur un delai borne dans le futur, sont decidables sur les automates hybrides fortement-non-zenon ; et qu'il est egalement decidable de verifier la qualite fortement-non-zenon pour un automate hybride quelconque. Enfin, nous presentons un logiciel de verification temporelle de programmes electre, base sur des algorithmes existants, et sur les resultats de decidabilite obtenus