中文摘要：

针对参数化系统验证面临的状态空间爆炸问题,提出自动抽象方法化简参数化系统状态空间.首先进行y-抽象建立单进程有限状态机模型,然后通过对多个y-抽象模型的合成运算得到异步合成的参数化系统,最后根据定义的谓词对参数化系统进行X-抽象得到二维抽象模型.运用该方法,对基于Synapse N＋1,Illinois,MESI,MOESI,Berkeley,Firefly和Dragon的7个参数化协议和注入错误的MESI协议进行自动化抽象建模,并验证了相关性质,有效地提升了验证参数化系统的能力、缩短了验证时间;应用文中方法验证FT-1000 CPU的一致性协议的结果表明,该方法在降低验证复杂度方面具有明显优势.

英文摘要：

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.