Sciweavers

Share
ICFEM
2010
Springer

Reasoning about Safety and Progress Using Contracts

8 years 11 months ago
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.
Imene Ben Hafaiedh, Susanne Graf, Sophie Quinton
Added 12 Feb 2011
Updated 12 Feb 2011
Type Journal
Year 2010
Where ICFEM
Authors Imene Ben Hafaiedh, Susanne Graf, Sophie Quinton
Comments (0)
books