基于时间自动机的实时系统形式化建模与验证

摘要

实时系统是一种带有时间约束的计算机系统．这些系统的许多动作的完成是与时间相关的，即要满足一定的时间限制。为了确保实时系统的正确性和可靠性，需要对其进行严格的分析和验证。实时系统的验证不仅要求逻辑上是正确的，而且要求时间上也是正确的。时间自动机是使用最为广泛的实时系统形式化建模工具。本文在R.Alur等人提出的时间自动机的基础上深入研究了实时系统建模与验证理论及其实际应用。 本文给出时间自动机的形式化定义，研究了基于时间自动机的实时系统建模方法，并给出了时间自动机模型的优化方法。最后对两个实时系统进行分析，利用时间自动机对它们建模。实时系统验证主要验证的问题分为安全性验证问题和活性验证问题，安全性验证问题可归结为时间自动机的可达性分析，由于模型检测方法在对系统验证时存在状态空间爆炸问题，因此，系统需要一种能较好解决该问题的自动规范验证技术。为了解决区域自动机构建过程中出现的状态空间爆炸问题，我们还引用了启发式验证方法。本文主要研究了基于历史等价和转换互模拟的最小化方法。经过最小化后，大大缓解了状态空间爆炸问题。 UPPAAL是一种以时间自动机作为行为模型的模型验证工具，它在实时系统的自动验证中占据重要位置。在对UPPAAL的基本结构和工作原理分析之后，我们发现它采用的限制技术和快速验证技术可以避免构建状态空间中的不可达状态，能在一定程度上解决状态空间爆炸问题。最后利用UPPAAL对已建立的两个实时系统的时间自动机模型进行性能验证，证明了它们的正确性和安全性。

目录

文摘

英文文摘

声明

第一章绪论

1.1研究背景

1.2研究现状

1.3研究内容

1.4本文组织结构

第二章基于时间自动机的形式化方法

2.1形式化建模

2.1.1时间自动机概述

2.1.2时间自动机模型

2.2形式化验证

2.2.1基于时间自动机的验证

2.2.2时间自动机验证工具UPPAAL

第三章基于时间自动机的实时系统建模

3.1实时系统概述

3.2实时系统的时间自动机建模

3.2.1转换系统

3.2.2有时间约束的转换系统

3.2.3实时系统时间自动机模型的优化

3.3应用实例分析

第四章基于时间自动机的实时系统验证

4.1基于时间自动机的实时系统验证方法

4.1.1区域自动机

4.1.2可达性分析

4.1.3启发式验证方法

4.2时间自动机验证工具UPPAAL的验证

4.3应用实例分析

第五章总结和展望

参考文献

攻读硕士期间发表(录用)的论文

致谢