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 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 informations that are not relevant for code generation.
展开▼
