Abstract FR:

Les travaux presentes ont pour objet la definition des bases formelles necessaires au developpement d'un systeme logiciel permettant la verification de machines sequentielles. La representation definie en logique temporelle par des formules valides elementaires permet de decrire le comportement des machines sequentielles; les regles d'unification de ces formules generent les comportements sur n'importe quel intervalle de temps: appeles evenements temporels. Ensuite, la definition formelle de la sensibilite d'un evenement temporel permet de generer des sequences de verification ou de demontrer des proprietes des machines considerees. Le memoire comporte les points suivants: 1) definition d'une representation symbolique de machines sequentielles en logique temporelle; 2) definition des formules representant la sensibilite, les conditions de sensibilite a une modification d'evenement temporel; 3) procedures d'etablissement de ces formules; 4) illustration de la generation de sequences (synchronisation, differenciation) et la demonstration de proprietes des machines (equivalence d'etats, machines minimales. . . )