@inproceedings{QG08a,
title = { Contract-Based Verification of Hierarchical Systems of Components },
author = {Quinton, Sophie and Graf, Susanne},
year = {2008},
booktitle = {6th IEEE Int. Conferences on Software Engineering and Formal Methods, SEFM08, Cape Town, South Africa, 10-14 November 2008},
pages = {377-388},
publisher = {IEEE Computer Society Press},
team = {DCS},
abstract = {We investigate contract-based verification of systems composed hierarchically from components by using glue operators from the BIP (Behavior, Interaction, Priority) framework. BIP builds on a clear separation between behavior of components and interaction between them. We extend the BIP framework by representing behaviors of atomic components as modal transition systems (MTSs) rather than LTSs. We introduce a notion of {\it contract} including a {\it structural} part and a {\it behavioral} part. The structural part of a contract $C$ for an interface $P_K$ describes the BIP interaction model $\gamma$ between $P$ and the environment $P_{Env}$ in which a component $K$ may be used. The behavioral part of $C$ consists of two MTSs: an {\it assumption} $A$ conforming to the interface $P_Env$, and a {\it guarantee} $G$ conforming to the interface $P_K$. Intuitively, $K$ -- defined by $(\gamma,B)$, $B$ a behaviour conforming to $P_K$ -- satisfies $C$ if as long as $Env$ behaves like $A$, $K$ behaves like $G$, where ``behaves like'' is defined with respect to $\gamma$. We explore a framework for compositional verification which decomposes verification of a global contract for a system made of $n$ components into $n$ verification problems of local contracts for the components, and refines the local contracts until either satisfaction or violation of the global contract can be proven. We provide several sufficient conditions for dominance between contracts (that is, satisfaction of a set of contracts implies satisfaction of another contract) based on circular reasoning. We also provide a satisfiability condition and an algorithm based on assumption generation to generate or refine contracts.},
}
