Représentation symbolique et vérification formelle de machines séquentielles / par Janine Magnier [née Clapier]

Date :

Editeur / Publisher : [S.l.] : [s.n.] , [1990]

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : français / French

Théorie des machines séquentielles

Théorie des automates mathématiques

Automatismes séquentiels

Essais (technologie)

Vérification (épistémologie)

Simulation, Méthodes de -- Logiciels

Générateurs (logiciels)

Machines logiques

Logique mathématique

Giambiasi, Norbert (1947-2016) (Directeur de thèse / thesis advisor)

Université des sciences et techniques de Montpellier 2 (1970-2014) (Organisme de soutenance / degree-grantor)

Résumé / Abstract : 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...)