论文部分内容阅读
模型检测是一种重要的形式化验证技术,能自动地检验系统是否满足所期望的性质。模型检测已经被成功地应用于计算机硬件、通信协议、控制系统和安全认证等方面的分析与验证中。模型检测面临的主要问题是状态空间爆炸问题,因为其是对状态空间的穷举搜索,对于并发系统,状态数随着并发分量的增加而呈指数级的增长。组合和抽象方法可以将系统抽象成一个有穷状态模型,去掉不影响待验证性质的细节,用尽可能少的状态描述系统运行过程。从而降低模型检测复杂性,在一定程度上缓解状态空间爆炸问题。本文提出了组合抽象框架,对框架做出理论分析,指出了框架的适应范围。通过建立各个主体的Kripke结构,扩展了组合抽象方法,基于LTL性质将其转化为抽象的Kripke结构,再组合抽象模型,最后运用模型检测工具Spin进行检测,以达到减少验证时产生的状态数的目的。详细分析了Promela模型的本身特点,通过对协议的Promela模型Spin模型检测,提出降低模型检测的复杂性方法。结果表明,组合抽象框架可以缓解状态空间爆炸问题,运用atomic和降低proctype进程的个数的方法,可以降低模型检测的复杂性。在以上工作的基础上,本文以NSPK协议为实例,建立了NSPK协议的Promela模型,运用Spin检测LTL性质,并对检测结果进行分析,指出了NSPK协议的缺陷,并且对修改后的NSPK也进行检测分析。对于多主体参与的协议,首先建立Kripke结构,再抽象组合,最后对比组合抽象前后状态数的变化,说明了组合抽象框架的可行性。对ATM自动取款机的UML模型检测时,将UML模型转化为Promela模型,在保证验证性质不变的情况下,运用组合抽象框架建立抽象的Promela模型,进一步说明了组合抽象框架的实用性。