Une approche multi-formalismes de spécification de systèmes répartis: Transformation de composants modulaires en réseaux de Petri

A. Diagne

LIP6 1997/007: THÈSE de DOCTORAT de l'UNIVERSITÉ PARIS 6 LIP6 / LIP6 research reports
226 pages - Juin/June 1997 - French document.

PostScript : 679 Ko /Kb

Contact : par mail / e-mail

Thème/Team: Systèmes Répartis et Coopératifs

Titre français : Une approche multi-formalismes de spécification de systèmes répartis: Transformation de composants modulaires en réseaux de Petri
Titre anglais : A Multi-Formalisms Approach for Distributed Systems Specification: Transformation of Modular Components into Petri Nets

Résumé : La spécification de systèmes répartis complexes et ouverts exige de gérer la qualité le long de leur cycle de vie et de disposer de référence commune permettant de les fédérer. Il faut donc avoir un support méthodologique et des méthodes formelles de vérification et de validation. Le support méthodologique peut être fourni par les méthodes orientées-objet de couverture du cycle de vie (de l'analyse à la réalisation) qui ont acquis un statut de standards commerciaux. Basé sur les mêmes concepts que ces méthodes, le modèle de référence des traitements répartis ouverts propose une base fédératrice de systèmes répartis ouverts.
La technologie objet et le modèle des traitements répartis ouverts offre une première base de fédération pour les faire coopérer en disposant de points de vue nécessaires à leur unification. Mais cette interopérabilité doit aussi obéir à des contraintes de sûreté et de fiabilité qui ne sont pas que du ressort de l'architecture fédératrice. En effet, le caractère critique de l'interopérabilité - entre systèmes ou composants d'un même système - dépend de la capacité de chacun à assurer le rôle qui lui est dévolu en respectant des propriétés locales dont dépend son fonctionnement et partiellement celui de son environnement. La formalisation et la vérification de telles propriétés font l'objet de cette thèse.
Parmi les nombreux critères de qualité, nous nous intéressons à ceux qui concernent le contrôle. Nous avons défini un modèle de composant basé-objet conforme aux principes de base du modèle de référence des traitements répartis ouverts. Ce modèle de composant permet en outre d'exprimer les aspects liés au contrôle dans les systèmes répartis de manière consistante pour des activités de vérification et de validation. Le modèle de composant est mis en correspondance de manière formelle avec un modèle de réseau de petri coloré modulaire. Sur le modèle modulaire de réseau de Petri, nous avons défini des algorithmes de vérification des principales propriétés de contrôle dans une approche d'évaluation de modèle (model checking). On peut vérifier la sûreté et la fiabilité dans une démarche incrémentale et en tirant profit de la modularité des composants pour éviter l'explosion combinatoire.

Abstract : Specification of complex open distributed systems needs to manage the quality along their life-cycle and to have a common reference in order to federate them. Therefore, a methodological support and formal methods of verification and validation are needed. The methodological support can be provided by commercial standard object-oriented methodologies which covers systems life-cycle (from analysis down to implementation). Based upon the same concepts, the Reference Model of Open Distributed Programming (RM-ODP) proposes a federative basis for open distributed systems.
Object technology and RM-ODP give a ground level to federate and make open distributed systems cooperate by supplying viewpoints necessary to unify them. But this interworking must obey safety and reliability constraints which are beyond the scope of the federative architecture. Actually, the dependability in interworking - between systems or components of a system - relies on the capability of each one to assume a role while preserving local properties which ensures correctness of its operating and thus partially the correctness of the environment operating. Formalization and verification of such properties is the purpose of this thesis.
Among the many properties relevant to quality for an open distributed system, we focus on those related to the control. We have defined an object-based component model compliant with the basic principles of the RM-ODP. This component model allows to express control aspects of a system in a way consistent for verification and validation activities. Its is transformed formally and automatically in a colored Petri net modular model. On the modular colored net model, we have defined algorithms to verify the most important control properties in a model-checking approach. Safety and reliability can be checked in an incremental approach with the benefits from modularity which allow to avoid state explosion.

Mots-clés : Systèmes Répartis, Spécification, Orientation-objet, Approches Multi-formalismes, RM-ODP, Réseaux de Petri colorés, Vérification, Validation

Key-words : Distributed Systems, Object-orientation, Multi-formalisms Approach, RM-ODP, Colored Petri nets, Verification, Validation

Publications internes LIP6 1997 / LIP6 research reports 1997

Responsable Éditorial / Editor
webmaster@lip6.fr