MODEL CHECKING AND MODULAR VERIFICATION

We describe a framework for compositional verification of finite-state processes. The framework is based on two ideas: a subset of the logic CTL for which satisfaction is preserved under composition, and a preo rder on structures which captures the relation between a component and a system containing the component. Satisfaction of a formula in the l ogic corresponds to being below a particular structure (a tableau for the formula) in the preorder. We show how to do assume-guarantee-style reasoning within this framework. Additionally, we demonstrate efficie nt methods for model checking in the logic and for checking the preord er in several special cases. We have implemented a system based on the se methods, and we use it to give a compositional verification of a CP U controller.