Parameterized Model Checking by enhancing the SPIN checker

Parameterized systems are characterized by the presence of a large (or even unbounded) number of behaviorally similar processes, and they often appear in distributed controllers and protocols. Verification of parameterized systems involves reasoning about unboundedly many processes and hence cannot be accomplished directly by model checking. In this work, we develop an abstraction refinement based verification framework for parameterized systems. We enhance the well-known SPIN model checker with process count abstractions to develop a time and memory efficient Linear-time Temporal Logic (LTL) model checker for parameterized systems. We also develop methods for automated detection of spurious counter-examples, and their elimination via abstrac-tion refinement. The usability / scalability of our checker is demonstrated via the modeling and automated verification of several real-life parameterized control systems and protocols