img

Notice détaillée

Modéles algébriques pour le parallélisme vrai et le raffinement d'actions

Thèses / mémoires Ecrit par: De-Simone, Robert ; Mery, Dominique ; Dekdouk, Abdelkader ; Dssouli, Rachida ; Publié en: 1997

Résumé: Le cadre général de mon travail de thèse est la théorie des processus. Pour être un peu plus précis, il s'inscrit dans le cadre de l'algèbre de processus. Son objectif, est de définir dans un premier temps des modèles algébriques de parallélisme vrai. Ensuite, étendre ces modèles avec le concept de raffinement d'actions. Initialement nous définissons deux sémantiques opérationnelles de parallélisme vrai pour un langage à la ACP. La première exploite la structure causale du processus et la deuxième repose sur l'hypothèse de la durabilité abstraite des occurrences d'action. Ensuite, nous établissons leurs modèles algébriques correspondants tout en respectant la propriété de correction et de complétude du dernier par rapport au premier. Les modèles définis représentent en fait des algèbres de processus. Par conséquent, cela nous fournit des formalismes de description explicite du parallélisme vrai, en plus de l'outil de vérification algébrique. La deuxième étape de ce travail consiste en la définition sémantique de l'opérateur de raffinement d'actions au sein des deux modèles définis, causal et ST. L'opérateur de raffinement d'actions permet de relier des spécifications à des niveaux différents d'abstraction, en implantant une action abstraite par une activité concrète. Il introduit par conséquent la notion de conception verticale qui est très importante pour la conception des systèmes d'actions. Finalement nous étendons les deux modèles algébriques incluant le raffinement d'actions avec le mécanisme d'abstraction des actions inobservables, en suivant les principes fondamentaux établis par l'équivalence observationnelle de Milner et l'équivalence de branchement de Van Glabbeek et Weijland, sachant que ce mécanisme d'abstraction représente un outil crucial pour la vérification des systèmes réactifs.

Nancy:
Langue: Français
Collation: 126 p. ill. ;30 cm.
Diplôme: Doctorat
Etablissement de soutenance: Nancy, Université Henri Poincaré. Faculté des sciences et techniques
Spécialité: Informatique
Index décimal 621 .Physique appliquée (électrotechnique, génie civil, génie mécanique, ingénierie appliquée, principes physiques en ingénierie)
Thème Informatique

Mots clés:
Systèmes, Théorie des
Parallélisme (Informatique)
Causalité (physique)
Simulation, Méthodes de
Langages formels

Note: Bibliogr. pp.117-123

Modéles algébriques pour le parallélisme vrai et le raffinement d'actions

Sommaire