Verifying Correctness of Contract Decompositions

Abstract: The importance of verification in safety critical systems is well known. However, due to the complexity of verification, the task of formally verifying large safety-critical systems might prove computationally infeasible in many cases. Compositional verification is a technique aimed at enabling verification of large safety-critical systems. One of the ambitions of compositional verification is to verify each component of a system against its specification separately, in such a way that the entire system as a unit is verified implicitly. This is possible if all component specifications imply the system specification. The problem of proving this implication is referred to as proving compositionality. In the context of compositional verification, assume/guarantee-contracts have emerged as the prevailing method for ensuring compositionality. An assume/guarantee-contract is a form of contract which specifically details what behaviour a component assumes (or expects) from a user, and what behaviour that component guarantees based on the assumption. Nyberg, Westman, and Gurov presented a solution to the problem of proving compositionality, in the context of assume/guarantee-contracts. The paper provides theory, such as a natural deduction system, for proving that a decomposed system does indeed satisfy the top level specification. This thesis explores how the pro cess of proving compositionality can be simplified, and formalizes the system developed by Nyberg, Westman, and Gurov in the interactive theorem prover HOL4. The work is presented as two HOL4 theories. The first theory is a complete formalization of the theory developed by Nyberg, Westman, and Gurov. Additionally, the HOL4 theory implicitly proves the correctness of the natural deduction system. The second theory is a formalization of a Gentzenstyle system. The theory implements the resulting system when translating the original natural deduction system to into a Gentzen-style system. While the first theory resulted in a feasible tool for proving compositionality interactively, as well as proving the original theory, it did not perform well when tasking HOL4 with finding proofs automatically. The second theory, the Gentzen-style system, performed much faster with automated reasoners. As an additional contribution, a comparison between the rules for proving compositionality, and the rules for type-checking intersection types in typed lambda calculus, was made. It is shown that structural similarities exist, and that these could possibly be used for faster proof search in compositionality; however, it is reasoned that an isomorphism is not likely to exist.