Exploring the Limits of Parameterized System Verification
This thesis addresses the problem of verification of parameterized systems. A parameterized system is given by a system description containing some parameters that can be instantiated by different values, such that different parameter instantiations may lead to different finite-state systems. It is known that the general verification problem for parameterized systems is undecidable. A framework for modeling parameterized systems and for deriving a classification of subclasses is presented. This classification is used to investigate the boundary between decidable and a number of undecidable parameterized system classes. Moreover, a verification method for parameterized systems based on abstraction is given. This method can be used to verify liveness properties as well, by deriving fairness constraints from the concrete system. The method is implemented in a tool set called pax. These tools can be used to automatically compute abstractions of parameterized systems and to translate these constructed abstract systems to input languages of existing model-checkers. Applicability of the verification method is demonstrated by presenting a case study of a cache-coherence protocol, and proving both its safety and its liveness properties.