University of Oulu
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 behavior of the environment (the remainder of components of the systems).