Imene Ben-Hafaiedh, Susanne Graf and Sophie Quinton
A Contract Framework for Reasoning about Safety and Progress (2010)
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.
