Model checking parameterized process classes

Abstract

Systems consisting of large (or even unbounded) number of behaviorally similarprocesses communicating with each other are known as parameterized systems.Such systems are common in distributed computing and real-life software systems.Verifying properties for such systems involves reasoning about unboundedly manyprocesses and hence cannot be accomplished directly by model-checking.In this thesis, we present an abstraction re nement based veri cation frameworkfor parameterized systems. We enhance the well-known Spin model checker withprocess count abstraction to develop a time/memory e cient Linear-time TemporalLogic (LTL) veri er for parameterized systems. We also developed methods toautomatically detect spurious counter-examples and re ne the abstraction. The usability/ scalability of our checker is demonstrated via the modeling and automatedveri cation of several real-life parameterized control systems and protocols.