基于自动机理论的高效模型检验算法研究

发布时间：2017-05-19 16:08

  本文关键词：基于自动机理论的高效模型检验算法研究，，由笔耕文化传播整理发布。

【摘要】：模型检验是一种重要的自动化验证技术,基于状态遍历的思想穷举系统能够到达的所有状态,并在系统不满足指定的性质时提供反例。本文主要关注适用于软件系统的基于自动机理论的(显式)模型检验。给定一个系统模型,根据待检验性质的不同,需要采用不同的模型检验算法验证系统是否满足性质,主要包括可达性算法、精化检验算法和面向时序逻辑模型检验的空性检验算法等。其中,精化检验和空性检验算法中还存在不少困难和挑战：(1)精化检验算法依赖于自动机的子集构造,容易引起状态空间爆炸问题,是制约精化检验应用范围的一个重要原因；(2)当前精化检验主要面向并发系统,而对于更复杂的系统,例如带有时间约束的实时系统(通常用时间自动机表示),还没有成熟有效的算法能够支持其精化检验；(3)有穷自动机的空性检验算法已经发展得比较成熟,然而时间自动机的空性检验需要进一步考虑non-Zenoness问题(即在有限时间内不能发生无穷多事件),目前还没有高效的算法支持。针对上述困难和挑战,本文重点研究基于反链的精化检验算法、时间自动机的精化检验算法,以及提出了一种新的基于non-Zenoness的时间自动机空性检验算法,主要工作和贡献如下：1.针对精化检验算法中子集构造引起的状态空间爆炸问题,本文首次将反链的思想引入到三类当前主要的精化检验算法中,提出了基于反链的路径精化检验、稳定故障精化检验和故障-偏差精化检验算法,展示了如何消减满足反链关系的状态,并证明了这三个算法的正确性。实验表明,基于反链的精化检验算法性能大大优于不使用反链的精化检验算法,性能提升多达几十倍。2.本文首次提出了时间自动机的精化检验算法,即给定两个时间自动机,一个时间自动机的语言是否包含于另一个时间自动机。算法采用了时钟域抽象这种目前最有效的抽象方法,得到有穷状态空间,使算法能够真正应用于实际系统。算法还在一定程度上克服了时间自动机确定化的不可判定性问题,即用理论以及实验证明了在绝大部分实际情况下算法是可以停止的。此外,算法还利用基于反链和上下界模拟关系的优化方法进一步提高算法性能。从实验结果可以得出,算法在实际系统的验证中表现出了良好的性能。3.本文提出了一种新的基于non-Zenoness的时间自动机空性检验算法.目前已存在的其他空性检验算法由于在检验non-Zenoness时需要引入额外的时钟或者状态,使得状态空间大大增加,算法性能往往十分低下。本文定义了一类特殊的时间自动机CUB-TA,并且为其提出了一种无需引入其他状态或时钟的空性检验算法,因此具有较高的效率。在此基础上,本文又证明了任意时间自动机都能够转化为CUB-TA,并提出了快速的转化算法。实验表明,大部分实际系统本身就是CUB-TA,或者只需要很小的代价就能转换成CUB-TA,因此本文提出的算法非常具有实用性。此外,本文的算法性能在大部分情况下高于其他算法。4.模型检验的成功很大程度上得益于验证工具的支持。本文在模型验证工具PAT框架中实现了上述所有算法,并结合PAT工具本身对各种形式化建模语言和语言解析的支持,使得用户可以方便地建模实际系统和待检验性质,并进行有效的验证。
【关键词】：模型检验 自动机 精化检验 反链 时间自动机 空性检验 Non-Zenoness
【学位授予单位】：浙江大学
【学位级别】：博士
【学位授予年份】：2015
【分类号】：TP301.1
【目录】：

• 摘要4-6
• Abstract6-14
• 第1章 绪论14-25
• 1.1 形式化方法和模型检验14-16
• 1.2 基于自动机理论的模型检验算法16-22
• 1.2.1 可达性算法17-18
• 1.2.2 精化检验算法18-20
• 1.2.3 空性检验算法20-22
• 1.3 本文工作22-25
• 1.3.1 研究点和创新点22-24
• 1.3.2 组织架构24-25
• 第2章 模型检验研究基础与现状25-45
• 2.1 模型检验概述25-28
• 2.1.1 模型检验概念26-27
• 2.1.2 模型检验的本质27-28
• 2.2 模型检验中的建模方法研究现状28-30
• 2.2.1 系统建模28-29
• 2.2.2 性质建模29-30
• 2.3 模型检验算法研究现状30-37
• 2.3.1 符号化模型检验算法30-31
• 2.3.2 基于自动机理论的模型检验算法31-37
• 2.4 模型检验算法优化方法研究现状37-41
• 2.5 模型检验工具研究现状41-43
• 2.6 本章小结43-45
• 第3章 基于反链的精化检验算法45-63
• 3.1 引言45-46
• 3.2 相关工作46-47
• 3.3 基本定义47-48
• 3.3.1 精化检验基本定义47-48
• 3.4 基于反链的精化检验48-59
• 3.4.1 基于反链的路径精化检验48-51
• 3.4.2 基于反链的稳定故障精化检验51-55
• 3.4.3 基于反链的故障-偏差精化检验55-59
• 3.5 实验及结果分析59-60
• 3.6 本章小结60-63
• 第4章 时间自动机的精化检验算法63-87
• 4.1 引言63-65
• 4.2 相关工作65-66
• 4.3 基本定义66-68
• 4.4 时间系统的路径精化检验68-72
• 4.4.1 时间自动机的路径精化检验方法69-70
• 4.4.2 基于反链的时间自动机路径精化检验算法70-72
• 4.5 时间自动机的精化检验72-79
• 4.5.1 性质模型展开72-74
• 4.5.2 精化检验中的时钟域抽象74-77
• 4.5.3 基于模拟关系的状态空间消减77-79
• 4.6 时间自动机的精化检验算法79-81
• 4.7 实验及结果分析81-86
• 4.7.1 时间自动机路径精化检验实验结果81-82
• 4.7.2 时间自动机间的精化检验实验结果82-86
• 4.8 本章小结86-87
• 第5章 基于non-Zenoness的时间自动机空性检验算法87-108
• 5.1 引言87-89
• 5.2 理论基础和相关工作89-94
• 5.2.1 理论基础89-90
• 5.2.2 SNZ(Strongly non-Zeno)方法90-91
• 5.2.3 GZG(Guessing Zone Graph)方法91-93
• 5.2.4 其他方法93-94
• 5.3 时间自动机CUB-TA94-97
• 5.4 基于non-Zenoness的空性检验算法97-102
• 5.4.1 CUB-TA的空性检验算法97-98
• 5.4.2 将任意时间自动机转化为CUB-TA98-102
• 5.5 实验及结果分析102-107
• 5.6 本章小结107-108
• 第6章 总结与展望108-110
• 6.1 本文工作总结108-109
• 6.2 未来工作展望109-110
• 参考文献110-119
• 攻读博士学位期间主要科研成果119-120
• 致谢120-121
• 作者简历121

【参考文献】

中国期刊全文数据库 前1条

1 高晓宁;计算机软件可靠性分析及抗不可靠性方法[J];航空计算技术;2003年03期

  本文关键词：基于自动机理论的高效模型检验算法研究，由笔耕文化传播整理发布。

本文编号：379140