LIP6 1997/007
- Thèse
Une approche multi-formalismes de spécification de systèmes répartis: Transformation de composants modulaires en réseaux de Petri - A. Diagne
- 226 pages - 16/06/1997- document en - http://www.lip6.fr/lip6/reports/1997/lip6.1997.007.ps.tar.gz - 695 Ko
- Contact : Alioune.Diagne (at) nulllip6.fr
- Ancien Thème : SRC
- 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
- Directeur de la publication : Denis.Poitrenaud (at) nulllip6.fr
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.
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.