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

摘要

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