Sophie Quinton, Susanne Graf and Roberto Passerone
Contract-Based Reasoning for Component Systems with Complex Interactions (2010)
Contract-Based Reasoning for Component Systems with Complex Interactions (2010)
TR-2010-12.pdf
Keywords: refinement, interface theories, circular reasoning
Abstract: This paper analyzes various notions of refinement used in contract and interface theories. We define a generic component algebra and then focus on possible verification strategies and discuss their compositional properties. We study the relationship between refinement of open systems and refinement under context, and show that we can obtain stronger compositional results, known as circular reasoning, if we loosen their connection. The theoretical results are then presented in the context of two models derived from the SPEEDS HRC specification language, and we show how to combine partial tool chains for both frameworks into a complete tool chain for our methodology.
