A Component-based Framework for the Specification, Verification and Validation of Open Distributed Systems

A. Diagne, P. Estraillier

LIP6 1997/037: Rapport de Recherche LIP6 / LIP6 research reports
18 pages - Décembre/December 1997 - Document en anglais.

PostScript : 698 Ko /Kb

Contact : par mail / e-mail

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

Titre français : Un environnement à base de composant pour la spécification, la vérification et la validation de systèmes répartis ouverts
Titre anglais : A Component-based Framework for the Specification, Verification and Validation of Open Distributed Systems

Résumé : 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.

Abstract : Open distributed systems have inherent complexity related to their control that makes it necessary to have a component-based approach to each of the activities undertaken along their life-cycle. Such an approach allows to apply the divide and conquer principles. In this paper, we propose a framework to undertake the specification, the verification and the validation (V&V) of distributed systems based on those composition principles. The approach herein uses a specification model which allows to describe the components of a distributed system. This model focuses also on the description of the interactions between the components in order to compose them into (sub-)systems. The properties expected are described and verified in a compositional way from the components to the (sub-)systems. The specification model is automatically transformed into a V&V model which is a modular Petri net standing with an object-based semantics. The verification of the properties is performed by model-checking on the reachability graphs computed from these nets. Other Petri nets structural analysis tools can also be applied to these nets as far as they support modular approaches. The compositionality allows to infer global properties from modular ones. Based on the direct executability of nets, the specification models are made executable so that they can be validated by simulation. The formal specification of a system can be validated against its informal initial requirements while involving its end-users and owners. Specific scenarios can be animated on the V&V model. This allows to achieve traceability of the confidence levels between the different stages of the life-cycle

Mots-clés : Spécification de systèmes répartis ouverts, Réseaux de Petri, Logique Temporelle, Vérification, Validation

Key-words : Specification of Open Distributed Systems, Petri Nets, Temporal Logic, Verification, Validation

Publications internes LIP6 1997 / LIP6 research reports 1997

Responsable Éditorial / Editor
webmaster@lip6.fr