论文部分内容阅读
摘要：随着信息技术的发展，软硬件系统越来越复杂，其中软硬件系统设计的正确性至关重要。形式化验证方法在硬件设计和软件开发等领域发挥越来越重要的作用，成为模拟验证的重要补充。本文主要介绍了形式化验证方法的发展现状并对其发展进行展望。
关键词：形式化验证方法;软件设计;硬件验证;模型检测;定理证明
中图分类号：TP301 文献标识码：A
文章编号：1009-3044（2019）34-0239-02
1 概述
硬件和软件系统在规模和功能上的增长增加了复杂性，也增加了潜在错误的可能性，这些错误引起了金钱、时间上的损失，甚至会危及人们的生命。形式方法是用于软件和硬件系统的规范，开发和验证的特定类型的基于数学的技术，是改善和确保系统质量的重要方法。形式化方法在软件和硬件领域中的应用进展比较显著，引起了各个领域的注意[1]。形式化验证方法是形式化方法的一个重要的研究内容，本文主要对形式化验证方法进行探讨。
2 基本概念
2.1 形式化规范说明
形式化规范说明是明确的表达所要设计的系统的及其性质的过程。形式化规范说明的语言具有严格的数学语法和语义，避免了自然语言的歧义性和不精确性[2]。可以用来表达系统的性质：功能行为、时序行为、性能特征以及内部结构，力求达到无二义性、一致性和完整性。这些可以用一种或多种语言来描述。目前对行为性质的形式化规范说明技术已经很成熟。把不同的规范说明语言结合在一起对系统进行描述成为一种发展趋势;另外一种趋势是对系统的非行为方面：性能、实时限制、安全要求、结构设计等进行形式化描述。
不同的形式规范说明方式要求不同的形式化规范语言。下面是用于顺序和并发系统形式规范的常见方法及语言：
2.2 形式化验证
形式验证是使用正式的数学方法证明或反驳系统相对于某个正式规范或属性的预期算法的正确性的行为，形式验证要求产品的规范和实现均需要有严格的形式描述[2]，如图2所示。主要有两种方法，一类是以逻辑推理为基础，逻辑推理有se-quent calculus， resolution natural deduction，以及Hoare-logic等方法，统称为定理证明技术;另一类则以穷尽搜索为基础统称为模型检测。
2.2.1 定理证明
定理证明：先对系统及其性质进行抽取，表示成基于某种逻辑的命题、谓词、定理，在验证者的引导下，不断地对公理、以证明的定理施加推理规则，产生新的定理，直到推导出表达系统性质的公式，从而证明设计的系统满足该性质。现在定理证明器越来越多的应用在验证硬件和软件设计的安全临界性质的验证[3]。
定理证明高度抽象，具有强大的逻辑表达能力，可以验证几乎所有的系统行为特性，可以处理无限的状态空间。定理证明器可以分为三种：自动定理证明器、交互式定理证明器及证明检验器。现在大多数定理证明器是交互式的，需要人的引导，对验证者的要求有良好的数学经验。
主要的定理证明工具有：STeP（Stanford）、TLV、AL2（UT Aus-tin/CLI）、Coq、HOL（Cambridge）、Isabelle（Cambridge）、Larch、Nu-prl、PVS（SRI）等。
2.2.2 模型检测
模型检测是建立一个系统的有限状态模型并检测希望满足的性质在这个模型中是否成立的技术。
目前有两种主要模型检测技术：一种是时态模型检测，这种方法中规范说明用时态逻辑公式表示，系统用有限状态转换模型表示，用模型检测器检测模型是否满足规范说明公式。另外一种是等价性检測，这种方法中规范说明用一个自动机表示，系统用一个自动机表示，然后证明两个模型是否一致。
自动化程度较高是模型检测的优点，并且当系统不满足给定的性质时，可以给出反例，使设计人员方便找出设计错误。模型检测应用于硬件和协议的验证，现在在对软件设计的验证已成为研究的热点。状态空间爆炸问题是其主要的缺点。
主要的模型检测工具有：COSPAN/FORMAL CHECK（Bell）、MURPHY（Stanford）、SPIN（Bell）、SMV（CMU）、VIS（Berkeley）等。
目前形式化验证方法成功应用于商业、航空业、通信业和芯片制造业，INTEL，ARM和NIVIDA等大公司已经把形式化方法应用到芯片的制造和验证[5]。
3 形式化验证方法的优缺点
3.1 形式化验证方法的优点
形式验证是完备的，能够完全断定设计的正确性，对指定描述得所有可能情况进行验证，不仅仅对其中的一个输入子集进行多次试验，克服了模拟实验的不足[4]。形式验证用数学方法将待验证电路与功能描述直接进行比较，不需要开发测试用例。形式化验证可以进行从系统级到门级的验证验证时间短，可以更早发现和改正设计缺陷，缩短周期和降低成本。形式验证工具能够自动验证特性的正确性，极大地方便了测试者，减小验证难度。形式验证工具应用断言验证的方法，断言以注释形式出现在代码中，从而既不影响原有代码的工作，又充分发挥了断言验证方法的作用，不影响原有验证流程。
3.2 形式化验证方法的不足
不管形式化验证是软件系统还是硬件设计，都要建立对象的各种模型，模型是在对原始设计进行抽象后所得到的，抽象出的模型和原始设计之间不可避免地存在鸿沟，而且验证的完整性取决于特性是否被全面准确的表达。形式化验证到目前为止仍然不能有效地的验证电路的性能，如电路的延时和功耗等[4]。当系统变复杂时，验证将占用较多的计算机资源，耗时增加。如前文所述各种形式化验证技术都有其固有的缺陷需要继续研究克服。
4 形式化验证方法发展的展望 形式化验证方法的主要目的是帮助设计人员设计更可靠的系统。形式化验证方法的进展依靠基础理论研究、研制新的方法和工具、方法和工具的集成等。主要从概念、方法和工具以及和其他技术结合等方面提出几点看法。
4.1 基本概念
形式化验证方法在实际应用中的显著作用依赖于计算机科学各个领域的研究结果。以后的工作主要包括以下范围：组织：必须对怎样组织方法、规范说明、模型、定理、证明等有深刻理解;分解：开发一种更有效地把全局的性质分解为更易验证的子性质的方法;抽象：不进行抽象很难对真实的系统进行规范和验证，对不同的系统或问题域采用不同的抽象技术;可复用模型和理论：对模型和理论进行复用可以减少工作量;数学理论的组合：很多安全临界系统既有数字元件也有模拟元件，这样的混合系统要求用离散和连续的数学理论进行推理;数据结构和算法：对大的搜索空间和大的系统进行处理时，就要求开发新的数据结构和算法。
4.2 方法和工具
为了吸引使用者，开发的工具和方法应满足以下特征：短的回收期、付出越多回报也越多、多用途、集成使用、易于使用、高效、易学、面向检错，聚焦分析、适应系统的发展等。没有任何一种方法或工具可以解决所有的问题，没有一种形式化工具可以描述和分析复杂系统的任何一个方面，因此把各种方法和工具集成起来使用成为一种趋势。主要是：模型检测和定理证明技术的集成、形式化规范与验证技术与传统的开发过程的集成、软件和硬件的设计验证方法的集成等。在软件工程中面向对象技术与形式方法相结合已经成为一个比较热的研究领域。形式化验证方法在以太坊智能合约安全监测中也得到广发应用。
5 结束语
本文主要探讨了形式化验证方法的有关基本概念，对形式化验证方法的两种主要形式：定理证明、模型检测进行阐述，以及从使用角度分析了形式化验证方法的优缺点，最后提出了对形式化验证方法的几点见解。
参考文献：
[1]韩俊刚，杜慧敏.数字硬件的形式化验证[M].北京大学出版社，北京：2001.12.
[2] CLARKE E M， WING J M. Formal Methods：State of the Artand Future Directions[Jl.ACM Computing Surveys，1996，28（4）.
[3] Johann M.Schumann， Automated Theorem Proving in SoftwareEngineering，Spring-Verlag 2001.
[4]张广泉.形式化方法导论[M].清华大学出版社，北京：2015.12.
[5]陈钢，于林宇，裘宗燕，等.基于逻辑的形式化验证方法：进展及应用[J].北京大学学报：自然科学版，2016，52（2）.
【通联编辑：王力】
收稿日期：2019-08-21
作者简介：陈波（1981-），女，山东淄博人，硕士，山东理工大学计算机科学与技术学院，讲师，研究方向为计算机软件与理論。
关键词：形式化验证方法;软件设计;硬件验证;模型检测;定理证明
中图分类号：TP301 文献标识码：A
文章编号：1009-3044（2019）34-0239-02
1 概述
硬件和软件系统在规模和功能上的增长增加了复杂性，也增加了潜在错误的可能性，这些错误引起了金钱、时间上的损失，甚至会危及人们的生命。形式方法是用于软件和硬件系统的规范，开发和验证的特定类型的基于数学的技术，是改善和确保系统质量的重要方法。形式化方法在软件和硬件领域中的应用进展比较显著，引起了各个领域的注意[1]。形式化验证方法是形式化方法的一个重要的研究内容，本文主要对形式化验证方法进行探讨。
2 基本概念
2.1 形式化规范说明
形式化规范说明是明确的表达所要设计的系统的及其性质的过程。形式化规范说明的语言具有严格的数学语法和语义，避免了自然语言的歧义性和不精确性[2]。可以用来表达系统的性质：功能行为、时序行为、性能特征以及内部结构，力求达到无二义性、一致性和完整性。这些可以用一种或多种语言来描述。目前对行为性质的形式化规范说明技术已经很成熟。把不同的规范说明语言结合在一起对系统进行描述成为一种发展趋势;另外一种趋势是对系统的非行为方面：性能、实时限制、安全要求、结构设计等进行形式化描述。
不同的形式规范说明方式要求不同的形式化规范语言。下面是用于顺序和并发系统形式规范的常见方法及语言：
2.2 形式化验证
形式验证是使用正式的数学方法证明或反驳系统相对于某个正式规范或属性的预期算法的正确性的行为，形式验证要求产品的规范和实现均需要有严格的形式描述[2]，如图2所示。主要有两种方法，一类是以逻辑推理为基础，逻辑推理有se-quent calculus， resolution natural deduction，以及Hoare-logic等方法，统称为定理证明技术;另一类则以穷尽搜索为基础统称为模型检测。
2.2.1 定理证明
定理证明：先对系统及其性质进行抽取，表示成基于某种逻辑的命题、谓词、定理，在验证者的引导下，不断地对公理、以证明的定理施加推理规则，产生新的定理，直到推导出表达系统性质的公式，从而证明设计的系统满足该性质。现在定理证明器越来越多的应用在验证硬件和软件设计的安全临界性质的验证[3]。
定理证明高度抽象，具有强大的逻辑表达能力，可以验证几乎所有的系统行为特性，可以处理无限的状态空间。定理证明器可以分为三种：自动定理证明器、交互式定理证明器及证明检验器。现在大多数定理证明器是交互式的，需要人的引导，对验证者的要求有良好的数学经验。
主要的定理证明工具有：STeP（Stanford）、TLV、AL2（UT Aus-tin/CLI）、Coq、HOL（Cambridge）、Isabelle（Cambridge）、Larch、Nu-prl、PVS（SRI）等。
2.2.2 模型检测
模型检测是建立一个系统的有限状态模型并检测希望满足的性质在这个模型中是否成立的技术。
目前有两种主要模型检测技术：一种是时态模型检测，这种方法中规范说明用时态逻辑公式表示，系统用有限状态转换模型表示，用模型检测器检测模型是否满足规范说明公式。另外一种是等价性检測，这种方法中规范说明用一个自动机表示，系统用一个自动机表示，然后证明两个模型是否一致。
自动化程度较高是模型检测的优点，并且当系统不满足给定的性质时，可以给出反例，使设计人员方便找出设计错误。模型检测应用于硬件和协议的验证，现在在对软件设计的验证已成为研究的热点。状态空间爆炸问题是其主要的缺点。
主要的模型检测工具有：COSPAN/FORMAL CHECK（Bell）、MURPHY（Stanford）、SPIN（Bell）、SMV（CMU）、VIS（Berkeley）等。
目前形式化验证方法成功应用于商业、航空业、通信业和芯片制造业，INTEL，ARM和NIVIDA等大公司已经把形式化方法应用到芯片的制造和验证[5]。
3 形式化验证方法的优缺点
3.1 形式化验证方法的优点
形式验证是完备的，能够完全断定设计的正确性，对指定描述得所有可能情况进行验证，不仅仅对其中的一个输入子集进行多次试验，克服了模拟实验的不足[4]。形式验证用数学方法将待验证电路与功能描述直接进行比较，不需要开发测试用例。形式化验证可以进行从系统级到门级的验证验证时间短，可以更早发现和改正设计缺陷，缩短周期和降低成本。形式验证工具能够自动验证特性的正确性，极大地方便了测试者，减小验证难度。形式验证工具应用断言验证的方法，断言以注释形式出现在代码中，从而既不影响原有代码的工作，又充分发挥了断言验证方法的作用，不影响原有验证流程。
3.2 形式化验证方法的不足
不管形式化验证是软件系统还是硬件设计，都要建立对象的各种模型，模型是在对原始设计进行抽象后所得到的，抽象出的模型和原始设计之间不可避免地存在鸿沟，而且验证的完整性取决于特性是否被全面准确的表达。形式化验证到目前为止仍然不能有效地的验证电路的性能，如电路的延时和功耗等[4]。当系统变复杂时，验证将占用较多的计算机资源，耗时增加。如前文所述各种形式化验证技术都有其固有的缺陷需要继续研究克服。
4 形式化验证方法发展的展望 形式化验证方法的主要目的是帮助设计人员设计更可靠的系统。形式化验证方法的进展依靠基础理论研究、研制新的方法和工具、方法和工具的集成等。主要从概念、方法和工具以及和其他技术结合等方面提出几点看法。
4.1 基本概念
形式化验证方法在实际应用中的显著作用依赖于计算机科学各个领域的研究结果。以后的工作主要包括以下范围：组织：必须对怎样组织方法、规范说明、模型、定理、证明等有深刻理解;分解：开发一种更有效地把全局的性质分解为更易验证的子性质的方法;抽象：不进行抽象很难对真实的系统进行规范和验证，对不同的系统或问题域采用不同的抽象技术;可复用模型和理论：对模型和理论进行复用可以减少工作量;数学理论的组合：很多安全临界系统既有数字元件也有模拟元件，这样的混合系统要求用离散和连续的数学理论进行推理;数据结构和算法：对大的搜索空间和大的系统进行处理时，就要求开发新的数据结构和算法。
4.2 方法和工具
为了吸引使用者，开发的工具和方法应满足以下特征：短的回收期、付出越多回报也越多、多用途、集成使用、易于使用、高效、易学、面向检错，聚焦分析、适应系统的发展等。没有任何一种方法或工具可以解决所有的问题，没有一种形式化工具可以描述和分析复杂系统的任何一个方面，因此把各种方法和工具集成起来使用成为一种趋势。主要是：模型检测和定理证明技术的集成、形式化规范与验证技术与传统的开发过程的集成、软件和硬件的设计验证方法的集成等。在软件工程中面向对象技术与形式方法相结合已经成为一个比较热的研究领域。形式化验证方法在以太坊智能合约安全监测中也得到广发应用。
5 结束语
本文主要探讨了形式化验证方法的有关基本概念，对形式化验证方法的两种主要形式：定理证明、模型检测进行阐述，以及从使用角度分析了形式化验证方法的优缺点，最后提出了对形式化验证方法的几点见解。
参考文献：
[1]韩俊刚，杜慧敏.数字硬件的形式化验证[M].北京大学出版社，北京：2001.12.
[2] CLARKE E M， WING J M. Formal Methods：State of the Artand Future Directions[Jl.ACM Computing Surveys，1996，28（4）.
[3] Johann M.Schumann， Automated Theorem Proving in SoftwareEngineering，Spring-Verlag 2001.
[4]张广泉.形式化方法导论[M].清华大学出版社，北京：2015.12.
[5]陈钢，于林宇，裘宗燕，等.基于逻辑的形式化验证方法：进展及应用[J].北京大学学报：自然科学版，2016，52（2）.
【通联编辑：王力】
收稿日期：2019-08-21
作者简介：陈波（1981-），女，山东淄博人，硕士，山东理工大学计算机科学与技术学院，讲师，研究方向为计算机软件与理論。