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