Technical Reports

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


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 | Site Map | Site powered by SPIP 4.2.13 + AHUNTSIC [CC License]

info visites 3974398