实时模型检测中精确加速的研究

论文摘要

实时系统经常会出现不同的时间度量。然而,当这些系统建模成时间自动机,然后运用符号模型检测技术进行验证时,验证速度会由于不必要的符号状态空间分裂(片段问题)而明显下降。精确加速可以解决由于不同时间度量而造成的模型检测时出现的片段问题,而且它不改变时间自动机的可达性,并可以有效地加速前向符号可达性分析。本文中,我们对精确加速原理进行了剖析,提出了一种基于驻留环实现精确加速的方法,解决了原来精确加速中附加环的大小需要依赖于可加速环窗口的问题,使得时间自动机精确加速模型的构造更加的简单快捷。同时我们还利用得出的推论,探讨了一种快速计算驻留环边界条件的方法,虽延时了加速的时机,但避免了可加速环窗口的复杂计算。此外,为了实现精确加速,还提出了一种识别时间自动机中可加速环的方法。针对时间自动机规模较大的问题,在识别可加速环的方法中引入拓扑排序的思想,通过简化时间自动机的规模,提高了识别时间自动机中可加速环的效率。通过实例验证和复杂度分析说明该方法是可行的。

论文目录

• 摘要
• ABSTRACT
• 1 引言
• 1.1 研究背景
• 1.2 研究现状
• 1.3 研究内容
• 1.4 本文结构
• 2 时间自动机
• 2.1 相关背景
• 2.2 时间自动机
• 2.3 区域自动机
• 2.3.1 区域等价
• 2.3.2 区域自动机
• 2.4 带自动机
• 2.5 可达性分析
• 2.6 小结
• 3 加速技术分析
• 3.1 片段问题
• 3.2 模型增量
• 3.3 精确加速
• 3.3.1 环
• 3.3.2 可加速环
• 3.3.3 加速
• 3.4 加速技术分析
• 3.5 小结
• 4 基于驻留环的精确加速
• 4.1 精确加速缺陷分析
• 4.2 精确加速原理分析
• 4.3 基于驻留环的精确加速
• 4.4 对比分析
• 4.5 小结
• 5 一种快速计算边界控制条件的方法
• 5.1 窗口的计算
• 5.2 一种快速计算边界控制条件的方法
• 5.3 实例验证及分析
• 5.4 小结
• 6 一种识别可加速环的方法
• 6.1 相关背景
• 6.2 模型检测工具UPPAAL
• 6.2.1 用UPPAAL建模
• 6.2.2 用UPPAAL检测
• 6.3 可加速环识别算法
• 6.4 实例验证及复杂度分析
• 6.5 小结
• 7 总结与展望
• 参考文献
• 致谢
• 个人简历 在学期间发表的学术论文与研究成果