LIP6 1997/039
- Reports
Depuis les Spécifications Formelles à l'Implémentation de Systèmes Répartis: Une approche Multi-Formalisme - A. Diagne, F. Kordon
- 22 pages - 12/19/1997- document en - http://www.lip6.fr/lip6/reports/1997/lip6.1997.039.ps.gz - 96 Ko
- Contact : Alioune.Diagne (at) nulllip6.fr, Fabrice.Kordon (at) nulllip6.fr
- Ancien Thème : SRC
- Keywords : Formal Specification, Petri Nets, Validation, Verification, Design Traceability, Prototyping, Distributed Systems
- Publisher : Denis.Poitrenaud (at) nulllip6.fr
This paper proposes a methodology to build safe distributed systems that considers both conceptual and operational description aspects. At the conceptual level, we focus on the safety and liveness properties expected from the system. Such properties are stated and then verified. At the operational level, we focus on properties addressing the optimization of the generated code. Traceability between the two levels is managed in a satisfactory semi-automatic way. It preserves the properties proved at the first level and discards information that are not relevant for code generation. The paper presents the general methodology and proposes an application to a simple example.