Contract-Based Verification of Hierarchical Systems of Components

In this paper, we add to the usual notion of contract a structural part specifying the composition operator used to compose the component and its environment. We provide a framework for compositional verification including a proof rule for dominance between contracts based on apparent circular reasoning. We also briefly describe a consistency condition and a method based on assumption generation to generate or refine contracts.