Verimag

Technical Reports

Imene Ben-Hafaiedh, Susanne Graf and Sophie Quinton
A Contract Framework for Reasoning about Safety and Progress (2010)

TR-2010-11.pdf


Keywords: contracts component-based systems incremental verification compositional verification

Abstract: Designing concurrent or distributed systems with complex architectures while preserving a set of high-level requirements through all design steps is not a trivial task. An approach which is both compositional and incremental is mandatory to master this complexity. We propose here a contract-based design and verification framework for safety and progress requirements in component systems with data exchange. We build upon a notion of contract framework which relies on a component algebra and two refinement relations: conformance and refinement under context. We provide a condition under which circular reasoning can be used for checking dominance, i.e. refinement between contracts. We illustrate our verification methodology with a case study: a protocol for tree-like networks for which both safety and progress must be ensured.

Contact | Plan du site | Site réalisé avec SPIP 3.0.26 + AHUNTSIC [CC License]

info visites 876289