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

• 作者: 屈婉霞 张龙 李思昆 郭阳
• 来源期刊: 计算机辅助设计与图形学学报
• 学科: 工学
• 关键词: 参数化系统 模型检验 二维抽象 有限状态机
• 年，卷（期）: 2014,（6）
• 所属期刊栏目: VLSI设计与测试及电子设计自动化
• 页码范围: 991-998
• 页数: 8页
• 分类号: TP302
• 字数: 6117字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	郭阳	国防科学技术大学计算机学院	39	252	9.0	14.0
2	李思昆	国防科学技术大学计算机学院	133	1339	18.0	31.0
3	张龙	国防科学技术大学计算机学院	4	13	2.0	3.0
4	屈婉霞	国防科学技术大学计算机学院	8	88	5.0	8.0