You Assume, We Guarantee: Methodology and Case Studies

. Assume-guarantee reasoning has long been advertised as the method for decomposing proof obligations in system verification. Refinement mappings (homomorphisms) have long been advertised as the method for solving the language-inclusion problem in practice. When confronted with large verification problems, we therefore attempted to make use of both techniques. We soon found that rather than offering instant solutions, the success of assume-guarantee reasoning depends critically on the construction of suitable abstraction modules, and the success of refinement checking depends critically on the construction of suitable witness modules. Moreover, as abstractions need to be witnessed, and witnesses abstracted, the process must be iterated. We present here the main lessons we learned from our experiments, in form of a systematic and structured discipline for compositional verification of fair reactive modules. This discipline has succeeded in several major case studies, of which we discuss..