Reasoning about Safety and Progress Using Contracts

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. Building upon a generic notion of contract framework which relies on a component framework 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 then propose an instantiation of such a contract framework for safety and progress requirements in component systems with data exchange. This allows us to prove non-trivial properties of a protocol for tree-like networks.

• Type: Journal
• Year: 2010
• Where: ICFEM
• Authors: Imene Ben Hafaiedh, Susanne Graf, Sophie Quinton
• Keywords: CONTRACT Framework, ICFEM 2010, Refinement Relations, Software Engineering, Trivial Task