Computing Invariants for Parameter Abstraction

A new approach to combining invariants computing and guard strengthening methods is presented in the context of parameter abstraction for parameterized model checking of cache coherence protocols. The approach uses a small instance of a parameterized protocol as a "reference model" to compute candidate invariants. References to a specific node in these candidate invariants are then abstracted away, and the resulting formulas are used to strengthen guards of the transition rules in the abstract node. The correctness of the approach is guaranteed by symmetry which exists in many parameterized systems. A number of case studies have been carried out to illustrate the effectiveness of the approach. During the process a data consistency error was identified and fixed in the German 2004 cache coherence protocol.