Titre:
Algebraic Models for True Parallelism and Action Refinement
Conférencier:
Abdelkader Dekdouk ,
stagiaire postdoctoral
Departement d'informatique et de recherche operationnelle
Universite de Montréal
Lieu:
Université de Montréal, Pavillon André-Aisenstadt ,
Salle 3195
Date et heure:
lundi le 04 mai 1998 de
14:00 à 00:00
Résumé:
The talk I will present is very close to my Ph.D. thesis work that fits into the process algebra framework. Its goal is twofold. First, to define algebraic models for true concurrency and second, to extend these models with action refinement concept.
We begin by defining two operational models of true concurrency for an extension of ACP 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 process 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 finalize this work by enriching both the true-concurrent models including action refinement with the mechanism of abstraction w.r.to 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.
N.B. La presentation sera faite en anglais.
Note biographique: Abdelkader Dekdouk est ne a Oran (Algerie) le 1er aout 1969. Il a obtenu son diplome d'Ingenieur en Informatique a l'Universite d'Oran, en 1992, ensuite les diplomes de DEA et de Doctorat en Informatique a l'Universite de Nancy (1993 et 1997). Actuellement il occupe un poste de stagiaire postdoctoral a l'Universite de Montreal, au Departement d'Informatique et de Recherche Operationnelle. Il travaille sur la specification et verification des systemes numeriques, dans le groupe de recherche dirige par le Prof. Eduard Cerny.