面向参数化系统验证的自动抽象方法  

Automatic Abstraction for Verification of Parameterized Systems

作　　者：张龙[1] 屈婉霞[1] 郭阳[1] 李思昆[1] 

机构地区：[1]国防科学技术大学计算机学院,长沙410073

出　　处：《计算机辅助设计与图形学学报》2014年第6期991-998,共8页Journal of Computer-Aided Design & Computer Graphics

基　　金：国家自然科学基金重点项目(61133007)

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

关 键 词：参数化系统 模型检验 二维抽象 有限状态机 

分 类 号：TP302[自动化与计算机技术—计算机系统结构]