Rajeev Alur, Luca de Alfaro, Thomas A. Henzinger, and Freddy Y.C. Mang
Modular verification techniques attempt to overcome the state-explosion problem occurring in the analysis of large systems by exploiting the modular structure naturally present in most system designs. Unlike other tasks in the verification of finite-state systems, current modular verification techniques rely heavily on user guidance. In this paper, we present an approach to modular verification that is almost entirely automatic, leaving to the user only the task of specifying which parts of a module should be visible from the other modules in the verification process. The proposed approach replaces in the verification process the concrete modules composing the system with abstract modules. The abstract models are constructed automatically, using reachability and controllability information about the concrete modules. Our experimental results indicate that the reachability and controllability information used in the construction of the abstractions enables the use of abstractions that are often much smaller than the original modules, drastically reducing the space and time requirements for verification.
Proceedings of the Tenth International Conference on Concurrency Theory (CONCUR), Lecture Notes in Computer Science 1664, Springer, 1999, pp. 82-97.