3.1.1　软件形式化测试概述

形式化方法源于Dijkstra和Hoare的程序验证。针对形式化方法的研究已经有几十年，但目前仍没有统一的对形式化方法的定义，Encyclopedia of Software Engineering一书对形式化方法的定义为：“用于开发计算机系统的形式化方法是基于数学的用于描述系统性质的技术。这样的形式化方法提供了一个框架，人们可以在该框架中以系统的方式刻画、开发和验证系统。”通常，凡是采用严格的数学工具、具有精确数学语义的方法，都可以称为形式化方法。形式化方法的一种分类方法如表3-1所示。

形式化方法在通信协议以及嵌入式软件建模及测试中已取得较多研究成果，且已被越来越多地应用于安全关键软件验证领域。欧洲航天局和NASA对于安全关键软件的开发高度推荐使用形式化方法。在实际应用中，实时嵌入式软件往往是安全关键软件，因此，在实时嵌入式软件系统测试中采用形式化方法可以消除二义性，增强测试的准确性和一致性，提高测试的自动化程度和测试效率。

从国内外的技术发展和研究来看，目前基于形式化方法的软件建模及测试技术的研究领域总结如图3-1所示。