形式规范的自动验证算法的研究

摘要

形式化方式包括了形式规范和设计验证两个方面，它的目的是以数学的方式来对系统进行描述，为保证软件的可靠性提供条件。在现代软件系统开发过程当中，经常会要求在某些限定的时间约束之下，对系统的输入数据进行相应的处理，以及系统内部所进行的状态之间的变迁，最后给出对应的输出数据。
　　本文的主要工作如下：
　　本文首先介绍了一种结合接口自动机（Interface Automata）和Z语言的规范ZIA以及ZIAs之间的精化关系。然后研究了MARTE（Modeling and Analysis of Real-Time and Embedded Systems），它在UML的基础上对于时间以及其他方面进行了一定的扩充。MARTE定义了基于模型的实时和嵌入式系统描述的基础。本文详细描述了MARTE中的一些基本和核心概念。然后给出了一种基于离散时间的ZIA模型规范（DT-ZIA），它不仅能够描述某些实时系统中针对在离散时间下的时间约束的要求，同时能够对系统的数据处理和状态变迁进行精确的表达。接着是MARTE的六元组表示，再接着是MARTE到DT-ZIA的转换方法。最后我们给出了在有限定义域上的ZIAs精化检测算法（包括算法的数据结构和流程图）、面向带有数据约束的实时系统的时序逻辑和在有限定义域上的DT-ZIA模型检测算法（包括实现类图和流程图）以及两个算法的实例验证。

目录

封面

声明

中文摘要

英文摘要

目录

图表清单

缩略词

第一章 绪论

1.1 引言

1.2 嵌入式实时系统的建模与分析MARTE

1.3 软件规约方法和Z语言

1.4 接口自动机和时间自动机

1.5 模型检测

1.6 本文的主要研究内容和组织框架

第二章 带Z的接口自动机

2.1接口自动机(IA)

2.2 时间自动机

2.3 带Z的接口自动机(ZIA)

第三章 从MARTE到DT-ZIA的转换

3.1 MARTE

3.2 Z语言

3.3 UML到Z的转换

3.4基于离散时间的ZIA（DT-ZIA）

3.5 MARTE的六元组表示

3.6 MARTE到DT-ZIA的转换

第四章 检测算法和实例验证

4.1 ZIA精化检测算法

4.2 DT-ZIA模型检测算法

4.3 实例验证

第五章 总结和展望

5.1本文总结

5.2未来展望

参考文献

致谢

在学期间的研究成果及发表的学术论文