Automatic Abstraction for Verification of Parameterized Systems

This paper presents a novel automatic abstraction method to address the state explosion problem in the verification of parameterized systems.Firstly,a Y-abstraction model is constructed to model the finite state machine of a single component.Secondly,an asynchronous composition of multiple Y-abstraction models is built by the composition operation.Finally,with the predicates defined,we obtain the two-dimension abstraction model of the parameterized system by X-abstraction. By the automatic abstraction method,we have modeled and validated some parameterized cache coherence protocols like Synapse N+1,Illinois,MESI,MOESI,Berkeley,Firefly,Dragon,and MESI-e,a version of MESI protocol with errors injected manually.The proposed method effectively improves the capability to validate parameterized systems,and reduces the time of verification.The method is also used to verify the coherence protocol in FT-1000 CPU,and it shows the great advantages in reducing the verification complexity.