Date : 1995
Editeur / Publisher : [S.l.] : [s.n.] , 1995
Format : 250 P.
Type : Livre / Book
Type : Thèse / ThesisLangue / Language : français / French
Résumé / Abstract : LA MISE EN PLACE DE TECHNIQUES DE VERIFICATION DE PROGRAMME VHDL NECESSITE LA FORMALISATION DE LA SEMANTIQUE DU LANGAGE, AINSI QUE LE DEVELOPPEMENT D'OUTILS AUTOMATIQUES DE VERIFICATION DE PROPRIETES A PARTIR DU MODELE FORMEL. NOUS REDUISONS L'ANALYSE DU SYSTEME A SES ETATS OBSERVABLES, APPELES ETATS STABLES, ET DEFINISSONS LA SEMANTIQUE D'UN SOUS ENSEMBLE DE VHDL EN TERMES DE RESEAUX DE PETRI INTERPRETES ET TEMPORISES. DEUX MODELES DE TEMPS SONT PROPOSES: LE PREMIER, DETERMINISTE, PERMET DE REPRESENTER EXACTEMENT LES PARAMETRES TEMPORELS DU PROGRAMME VHDL. LE SECOND, INDETERMINISTE, PERMET DE REPRESENTER DES FAMILLES DE PROGRAMMES PARAMETRES EN TEMPS. L'APPLICATION DE REGLES DE REDUCTION PERMET DE MINIMISER LA TAILLE DU RESEAU DE PETRI TOUT EN PRESERVANT SA SEMANTIQUE. LE RESEAU DE PETRI OBTENU EST UN FORMALISME INTERMEDIAIRE PERMETTANT DE CONSTRUIRE DES SYSTEMES DE TRANSITIONS CARACTERISANT LE COMPORTEMENT DU PROGRAMME VHDL EN SES POINTS OBSERVABLES. UNE METHODE DE CONSTRUCTION DE L'ENSEMBLE DES ETATS STABLES EST PROPOSEE. ELLE ETEND L'ALGORITHME DE PARCOURS SYMBOLIQUE DU RESEAU DE PETRI PROPOSE PAR PASTOR ET. AL. EN 94, EN L'ADAPTANT AUX RESEAUX INTERPRETES ET TEMPORISES A DELAIS INDETERMINISTES, ET EN SE FOCALISANT SUR LES ETATS STABLES DU SYSTEME. UNE STRATEGIE DE REORDONNANCEMENT DYNAMIQUE DES BDD, BASEE SUR DES SEUILS D'INVOCATIONS, EST PRESENTEE ET EVALUEE. NOUS MONTRONS COMMENT LA PRISE EN COMPTE DU DETERMINISME DE VHDL'87 PERMET DE CONSTRUIRE DIRECTEMENT, A PARTIR DE LA STRUCTURE DU RESEAU DE PETRI, UN SYSTEME DE TRANSITIONS SYMBOLIQUE REPRESENTANT L'EXECUTION D'UN CYCLE DE SIMULATION. CETTE RELATION EST UTILISEE POUR VERIFIER DES PROPRIETES EXPRIMEES EN CTL, EN APPLIQUANT LES ALGORITHMES CLASSIQUES DE VERIFICATION DE MODELE SYMBOLIQUE. L'UTILISATION DES DIFFERENTS MODELES POUR LA VERIFICATION DE TELLES PROPRIETES EST ILLUSTREE ET COMPAREE SUR DE NOMBREUX EXEMPLES A L'AIDE DES OUTILS PROTOTYPES QUE NOUS AVONS REALISES. NOUS PROPOSONS EGALEMENT DE COMBINER L'ANALYSE STRUCTURELLE DU RESEAU DE PETRI ET LES TECHNIQUES DE VERIFICATION DE MODELE SYMBOLIQUE POUR DETECTER LES PROGRAMMES VHDL INSTABLES