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

Abstract : 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.
Document type :
Theses
File URL :
http://docnum.univ-lorraine.fr/prive/SCD_T_1997_0188_DEKDOUK.pdf
Complete list of metadatas

https://hal.univ-lorraine.fr/tel-01747400
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 10:58:47 AM
Last modification on : Tuesday, January 29, 2019 - 1:21:53 AM

Identifiers

  • HAL Id : tel-01747400, version 1

Collections

Citation

Abdelkader Dekdouk. Modèles algébriques pour le parallélisme vrai et le raffinement d'actions. Autre [cs.OH]. Université Henri Poincaré - Nancy 1, 1997. Français. ⟨NNT : 1997NAN10188⟩. ⟨tel-01747400⟩

Share

Metrics

Record views

8