Date : 1995
Editeur / Publisher : [S.l.] : [s.n.] , 1995
Format : 267 P.
Type : Livre / Book
Type : Thèse / ThesisLangue / Language : français / French
Résumé / Abstract : NOUS PRESENTONS PLUSIEURS CONTRIBUTIONS REALISEES DANS LE CADRE DU DEVELOPPEMENT D'UNE APPROCHE POUR LA VERIFICATION FORMELLE DE SYSTEMES PARALLELES. LA PREMIERE CONTRIBUTION EST UN OUTIL THEORIQUE DE MODELISATION, LES GRAPHES ABSTRAITS ANNOTES (GAA). CES OBJETS MATHEMATIQUES PERMETTENT DE MAINTENIR LA SEPARATION ENTRE LA STRUCTURE FINIE DES DESCRIPTIONS ET LEUR CONTENU SEMANTIQUE QUI EST GENERALEMENT INFINI. MALGRE LEUR RELATIVE SIMPLICITE THEORIQUE ILS CONSTITUENT UN MOYEN DE DESCRIPTION PARTICULIEREMENT PUISSANT ET ACCESSIBLE DE NOMBREUSES PROPRIETES SOPHISTIQUEES (E.G. COHERENCE GLOBALE, FRAICHEUR, AUTHENTIFICATION). LA DEUXIEME CONTRIBUTION EST RELATIVE A LA CONCEPTION D'UNE TECHNIQUE DE VERIFICATION PARTICULIEREMENT PUISSANTE QUI PERMET D'EXPLOITER L'ORDRE PARTIEL DES EVENEMENTS POUR REDUIRE A LA FOIS LA COMPLEXITE DE L'EXPRESSION D'INVARIANT ET CELLE DE LA VERIFICATION. LA TROISIEME CONTRIBUTION EST UNE APPLICATION AU DOMAINE DE LA VERIFICATION DES PROTOCOLES D'AUTHENTIFICATION. L'APPROCHE SEPARE LA MODELISATION DES CONNAISSANCES, DE LA MODELISATION DE NOTIONS DE NATURE TEMPORELLE COMME LA FRAICHEUR. CETTE APPROCHE EST ILLUSTREE POUR LA VERIFICATION D'UN PROTOCOLE D'AUTHENTIFICATION PARTICULIEREMENT REPRESENTATIF, CELUI DE NEEDHAM-SCHROEDER. LA QUATRIEME CONTRIBUTION EST UNE THEORIE SEMANTIQUE POUR L'UNIFICATION DES PARADIGMES DE PROGRAMMATION PARALLELE, FONCTIONNELLE ET IMPERATIVE. NOTRE THEORIE SEMANTIC EST COMPOSEE ESSENTIELLEMENT D'UNE SEMANTIQUE STATIQUE ET DE DEUX SEMANTIQUES DYNAMIQUES: L'UNE OPERATIONNELLE ET L'AUTRE DENOTATIONNELLE