Algebraic models for true-concurrency and action refinement
Modèles algébriques pour le parallélisme vrai et le raffinement d'actions
Résumé
This work fits into the process algebra framework. Its goal is twofold. Firstly, to define algebraic models for true-concurrency and secondly to extend these models with action refinement concept. We begin by defining two operational models of true-concurrency for an extension of an ACPlike language. True-concurrency of the first model rests on the causality principle and assumes instantaneity of action occurrences. While the second one is based on the ST idea assuming that action occurrences are durable. Then we establish for each operational model its corresponding algebraic model for which it is proved correct and complete. These models define pro cess algebras that provide formalisms to express explicitly a true-concurrent behaviour, in addition to their ability of algebraic verification. The second step of this work is the semantic definition of action refinement operator within both the defined causal and ST models. The action refinement operator permits to relate specifications at different levels of abstraction by implementing an abstract action with a concrete activity. Hence it introduces the notion of vertical modularity which is very relevant for the design of action systems. We finalise this work by enriching both the true-concurrent models including action refinement with the mechanism of abstraction w.r.t unobservable actions, following the abstraction principles stated by the observational equivalence of Milner and the branching equivalence of Van Glabbeek and Weijland. As far as we know this mechanism constitutes a crucial tool for the verification of reactive systems.
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.