LIP6 1997/037
- Rapports de recherche
Un environnement à base de composant pour la spécification, la vérification et la validation de systèmes répartis ouverts - A. Diagne, P. Estraillier
- 18 pages - 17/12/1997- document en - http://www.lip6.fr/lip6/reports/1997/lip6.1997.037.ps.gz - 714 Ko
- Contact : Alioune.Diagne (at) nulllip6.fr, Pascal.Estraillier (at) nulllip6.fr, Denis.Poitrenaud (at) nulllip6.fr
- Ancien Thème : SRC
- Mots clés : Spécification de systèmes répartis ouverts, Réseaux de Petri, Logique Temporelle, Vérification, Validation
- Directeur de la publication : Denis.Poitrenaud (at) nulllip6.fr
Les systèmes distribués ouverts ont une complexité inhérente due à leur controle et qui rend nécessaire une approche basée composant à chacune des activités entreprises le long de leur cycle de vie. Une telle approche permet d'appliquer le principe de "diviser pour maitriser". Dans cet article, nous proposons un environnement à base de composants pour entreprendre la spécification, la vérification et la validation (V&V) de systèmes répartis basé sur les principes de composition. L'approche ici proposée utilise un modèle de spécification qui permet de décrire les composants d'un système reprti. Ce modèle permet aussi de décrire les interactions entre les composants en vue de les composer pour construire des (sous-)systèmes. Les propriétés attendues du système sont exprimées sur les composants et vérifiées dans une approche compositionelle. Le modèle de spécification est traduit automatiquement en un modèle de V&V qui est un réseau de Petri modulaire avec une sémantique basée objet. La vérification des propriétés est faite par model-checking sur les graphes d'accessibilité construits à partir de ces réseaux modulaires. D'autres outils d'analyse structurelles des réseaux de Petri peuvent être utilisés s'ils supportent des approches modulaires. La compositionalité permet d'inférer des propriétés globales à partir des propriétés modulaires. Basée sur l'exécutabilité des réseaux de Petri, les modèles de spécification sont rendus simulables. La spécification formalisée d'un système peut être validée par rapport aux besoins initiaux que ce dernier doit satisfaire en impliquant les mandataires et les utilisateurs finaux. Des scénarii spécificques peuvent être animés sur le modèle de V&V. Ceci permet de tracer les niveaux de confiance entre les différentes phases du cyclme de vie.