Automatic generation of assumptions for modular verification of software specifications

Abstract

Model checking is a powerful automated technique mainly used for the verification of properties of reactive systems. In practice, model checkers are limited due to the state explosion problem. Modular verification based on the assume-guarantee paradigm mitigates this problem using a “divide and conquer” technique. Unfortunately, this approach is not automated, for the reason that the user must specify the environment model. In this paper, a novel technique is presented for automatically generating component assumptions based on the behaviour of the environment (the remainder of components of the systems). In a first phase, the environment of the component is computed using state space exploration techniques, and then the assumptions are generated as association rules of the component environment interface. This approach presents a number of advantages. Firstly, user assistance to specify assumptions is not necessary and assumption discharge is avoided. Secondly, the component assumptions are more restrictive and real, and therefore reduce the resources needed by the model checker. The technique is applied to the specification of a steam boiler system