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

摘要：

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

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

所属期刊栏目：26

分类号：TP302(计算技术、计算机技术)

资助基金：国家自然科学基金重点项目61133007

在线出版日期：2014-07-01（万方平台首次上网日期，不代表论文的发表时间）

页数：共8页

页码：991-998