形式化测试和训练方法

定义
形式化方法是一种用于构建计算机系统的技术，其本质是通过数学手段来描述系统的特性。此类方法提供了一种框架，使得系统可以以一种系统化而非个别的方式被刻画、开发和验证。当某一种技术具备坚实的数学理论基础时，即可称之为形式化的，通常以形式化规约语言作为表达方式。这一理论基础为一系列精确定义的概念提供了支撑，例如：一致性与完整性，以及规范的实现与正确性。形式化方法的核心在于利用数学工具来描述目标软件系统的属性。不同形式化方法所依赖的数学基础各不相同，有些基于集合论和一阶谓词演算（如Z语言和VDM），而另一些则建立在时态逻辑之上。实现这些方法需要借助于形式化规约语言的支持。

根据对目标软件系统进行说明的方式，形式化方法可分为两类：
1）面向模型的形式化方法。这类方法通过构建一个数学模型来描述系统的运行行为；
2）面向属性的形式化方法。这种方法通过阐述目标软件系统的各项属性来间接地定义其行为。

依据表达能力的不同，形式化方法可划分为五类：
1）基于模型的方法：通过明确状态和操作的定义建立系统模型（使系统从一种状态转移到另一种状态）。该方式虽可表达非功能性需求（如时间约束），但在并发性的表现上存在局限性。例如Z语言、VDM以及B方法等均属于此类；
2）基于逻辑的方法：利用逻辑语言描述系统预期的行为特征，包括底层规约、时序及可能性行为，并借助所选逻辑体系中的公理进行证明