LIP6 1997/007
- Thesis
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 - 06/16/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
- Keywords : Distributed Systems, Object-orientation, Multi-formalisms Approach, RM-ODP, Colored Petri nets, Verification, Validation
- Publisher : Denis.Poitrenaud (at) nulllip6.fr
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.
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.