文章目录
【1】 概述【2】基本概念【2.1】形式化规范说明【2.2】形式化验证【2.2.1】定理证明【2.2.2】模型检测Reference：后续待阅读资料【1】 概述
硬件和软件系统在规模和功能上的增长增加了复杂性，也 增加了潜在错误的可能性，这些错误引起了金钱、时间上的损 失，甚至会危及人们的生命。形式方法是用于软件和硬件系统 的规范，开发和验证的特定类型的基于数学的技术，是改善和 确保系统质量的重要方法。形式化方法在软件和硬件领域中 的应用进展比较显著，引起了各个领域的注意[1]。形式化验证 方法是形式化方法的一个重要的研究内容，本文主要对形式化 验证方法进行探讨。
形式化方法一般可分为形式化规范说明Formal Specification，和形式化验证Formal Verification。
Formal
Formal Specification 形式化规范说明Formal Verification 形式化验证Theorem Proving 定理检测（证明）/Deductive Verification 演绎检测Model Checking 模型检测Automated Test Case Generation 自动测试用例生成
【2】基本概念
【2.1】形式化规范说明
硬件和软件系统在规模和功能上的增长增加了复杂性，也 增加了潜在错误的可能性，这些错误引起了金钱、时间上的损 失，甚至会危及人们的生命。形式方法是用于软件和硬件系统 的规范，开发和验证的特定类型的基于数学的技术，是改善和 确保系统质量的重要方法。形式化方法在软件和硬件领域中 的应用进展比较显著，引起了各个领域的注意[1]。形式化验证 方法是形式化方法的一个重要的研究内容，本文主要对形式化 验证方法进行探讨。
【2.2】形式化验证
【2.2.1】定理证明
定理证明：先对系统及其性质进行抽取，表示成基于某种 逻辑的命题、谓词、定理，在验证者的引导下，不断地对公理、以 证明的定理施加推理规则，产生新的定理，直到推导出表达系 统性质的公式，从而证明设计的系统满足该性质。现在定理证 明器越来越多的应用在验证硬件和软件设计的安全临界性质 的验证[3]。 定理证明高度抽象，具有强大的逻辑表达能力，可以验证 几乎所有的系统行为特性，可以处理无限的状态空间。定理证 明器可以分为三种：自动定理证明器、交互式定理证明器及证 明检验器。现在大多数定理证明器是交互式的，需要人的引 导，对验证者的要求有良好的数学经验。 主要的定理证明工具有：STeP(Stanford)、TLV、AL2(UTAus⁃ tin/CLI)、Coq、HOL(Cambridge)、Isabelle(Cambridge)、Larch、Nu⁃ prl、PVS(SRI)等。
【2.2.2】模型检测
模型检测是一种通过对目标系统建立一个有限的模型，并在模型发生改变时，检测希望满足的性质，例如安全性和活性在该模型中是否成立、稳定的技术。
目前有两种主要模型检测技术：
一种是时态模型检测，这 种方法中规范说明用时态逻辑公式表示，系统用有限状态转换模型表示，用模型检测器检测模型是否满足规范说明公式。另外一种是等价性检测，这种方法中规范说明用一个自动机表示，系统用一个自动机表示，然后证明两个模型是否一致。
自动化程度较高是模型检测的优点，并且当系统不满足给 定的性质时，可以给出反例，使设计人员方便找出设计错误。 模型检测应用于硬件和协议的验证，现在在对软件设计的验证 已成为研究的热点。状态空间爆炸问题是其主要的缺点。
主要的模型检测工具有：
COSPAN/FORMALCHECK(Bell)、MURPHY(Stanford)、SPIN(Bell)、SMV(CMU)、VIS(Berkeley)等。
目前形式化验证方法成功应用于商业、航空业、通信业和 芯片制造业，INTEL,ARM和NIVIDA等大公司已经把形式化方法应用到芯片的制造和验证[5]。
从本质上讲，模型检测技术就是穷尽对状态空间的搜索，并通过模型的有限性来保证该搜索过程一定会终止。最初的模型检测应用在硬件和协议验证领域，十分成功，后来在软件系统的验证上也得到了广泛应用。
Reference：
[形式化验证方法浅析] 陈波1，李夫明2 (1.山东理工大 学 计算机科学与技术学院，山东 淄博255000； 2.山东理工大学 数学与统计学院，山东 淄博255000)**
后续待阅读资料
线性时序逻辑 /p-506137477.html
模型检测 /view/800eade45a8102d277a22f3a.html?fr=search
model checking overview and buchi automata and LTL /p-1003260979.html
如果觉得《形式化验证学习——什么是形式化？Formal》对你有帮助，请点赞、收藏，并留下你的观点哦！
