论文部分内容阅读
模型检测是一种自动完成性质验证的算法过程，模型检测器是模型检测算法的工具实现，可用来检验系统是否满足某些性质，如可达性、安全性等，可以及时发现问题，更改系统设计中的缺陷，避免不必要的损失。实时系统由于涉及并发、不确定性以及时间约束等因素，其设计的正确性很难把握，因此利用模型检测对其进行分析显得更为重要。
CTAV/Reach是一个基于离散时间自动机的实时系统模型检测工具，利用它可以对可达性、安全性等性质进行检测。实验表明该工具具有良好的检测效率。
本文给出了CTAV/Reach的设计框架，重点介绍了可达性检测算法的设计与实现，以及实现过程中采用的一些优化策略，包括活动时钟约减技术、LU抽象方法等，并研究对比了各种策略对检测效率的影响，实验表明这些优化策略明显加快了检测速度。CTAV/Reach的状态空间用二叉判定图实现，文中研究对比了不同的变量序对状态空间大小的影响。通过与另一个模型检测工具Rabbit的比较体现了CTAV/Reach对时钟常量取值的敏感度较低的特点。
本文还介绍了一个基于离散时间自动机的非空性检测工具CTAV/LTL，利用它可以进行LTL性质的检测。文中主要介绍了CTAV/LTL的状态空间展开算法与使用的数据结构，并与其它检测工具进行了实验比较，说明了CTAV/LTL良好的检测效率。