In this chapter we propose a rule unifying circular and non-circular assume-guarantee reasoning and show its interest for contract-based design and ver- ification. Our work was motivated by the need to combine, in the top-down method- ologyoftheFP7SPEEDSproject,partialtoolchainsfortwocomponentframeworks derived from the HRC model and using different refinement relations. While the L0 framework is based on a simple trace-based representation of behaviors and uses set operations for defining refinement, the more elaborated L1 framework offers the possibility to build systems of components with complex interactions. Our approach in L1 is based on circular reasoning and results in a method for checking contract dominance which does not require the explicit composition of contracts. In order to formally relate results obtained in L0 and L1, we provide a definition of the minimal concepts required by a consistent contract theory and propose abstract definitions which smoothly encompass hierarchical components. Finally, using our relaxed rule for circular reasoning, we show how to use together the L0 and L1 refinement rela- tions and as a result their respective tool chains.
['Susanne Graf', 'Roberto Passerone', 'Sophie Quinton']
Contract-Based Reasoning for Component Systems with Rich Interactions