论文部分内容阅读
模型检验是一种重要的自动化验证技术,基于状态遍历的思想穷举系统能够到达的所有状态,并在系统不满足指定的性质时提供反例。本文主要关注适用于软件系统的基于自动机理论的(显式)模型检验。给定一个系统模型,根据待检验性质的不同,需要采用不同的模型检验算法验证系统是否满足性质,主要包括可达性算法、精化检验算法和面向时序逻辑模型检验的空性检验算法等。其中,精化检验和空性检验算法中还存在不少困难和挑战：(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工具本身对各种形式化建模语言和语言解析的支持,使得用户可以方便地建模实际系统和待检验性质,并进行有效的验证。