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

摘要：

针对参数化系统验证的状态空间爆炸问题,本文提出自动抽象方法化简参数化系统状态空间.首先,进行Y-抽象建立单进程状态机模型,然后,通过对多个Y-抽象模型的合成运算得到异步合成的参数化系统,最后,根据定义的谓词对参数化系统进行X-抽象得到二维抽象(TDA)模型.本文运用该方法对基于Synapse N+1、Illinois、MESI、Berkeley和Dragon的5个参数化协议进行自动化抽象建模并验证了相关性质,有效地提升了验证参数化系统的能力.

关键词： 参数化系统 自动抽象方法 状态空间 二维抽象模型

作者: 张龙 屈婉霞 郭阳

作者单位: 国防科技大学计算机学院,长沙410073

会议类型: 国内会议

会议名称: 第十七届全国计算机辅助设计与图形学学术会议(CAD/CG’ 2012)暨第九届全国智能CAD与数字娱乐学术会议(CID’ 2012)

会议地点: 青岛

会议语种:中文

页码: 359-362

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