LIP6 1997/037

• Reports
  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 - 12/17/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
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
• Keywords : Specification of Open Distributed Systems, Petri Nets, Temporal Logic, Verification, Validation
• Publisher : Denis.Poitrenaud (at) nulllip6.fr