The Wayback Machine - https://web.archive.org/web/20221028225800/https://baike.sogou.com/kexue/d10376.htm

形式验证

编辑

在硬件和软件系统设计过程中，形式验证是使用数学的方法，证明或否定系统基础上的特定形式规范或属性的预期算法的正确性的行为。[1]

形式验证有助于证明系统的正确性，例如：密码协议、组合电路、具有内部存储器的数字电路和表示为源代码的软件。

这些系统的验证是通过对系统的抽象数学模型、数学模型与结构已知系统性质之间的对应关系提供正式证明来完成的。常用于系统建模的数学对象的例子有：有限状态机、变迁系统、佩特里网、向量加法系统、时间自动机、混合自动机、过程代数、编程语言的形式语义，如操作语义、指称语义、公理语义和霍尔逻辑。[2]

1 方法编辑

一种方法和形式是模型检查，它包括对数学模型的系统详尽的探索（这对于有限模型是可能的，但对于某些无限模型也是可能的，在这些无限模型中，通过使用抽象或利用对称性可以有限地有效地表示无限组状态）。通常这包括探索模型中的所有状态和转换，通过使用智能和特定于领域的抽象技术来考虑单个操作中的整个状态组，并减少计算时间。实现技术包括状态空间枚举、符号状态空间枚举、抽象释义、符号模拟、抽象细化。需要验证的属性通常在时间逻辑中描述，例如线性时间逻辑（LTL）、属性说明语言（PSL）、系统验证日志断言（SVA）、[3] 或计算树逻辑（CTL）。模型检查的最大优点是它通常是全自动的；它的主要缺点是它一般不能扩展到大型系统；符号模型通常限于几百位状态，而显式状态枚举要求正在探索的状态空间相对较小。

另一种方法是演绎验证。它包括从系统及其规范（以及可能的其他注释）生成一组数学证明义务，其真实性意味着系统符合其规范，并使用交互式定理证明器（如HOL、ACL2、Isabelle、Coq或PVS）、自动定理证明器或可满足性模理论（SMT）解算器来履行这些义务。这种方法的缺点是，它通常要求用户详细理解系统为什幺正确工作，并且以待证明的定理序列的形式或者以系统组件（例如函数或过程）以及可能的子组件（例如循环或数据结构）的规范的形式将该信息传送给验证系统。

1.1 软件

软件程序的正式验证包括证明一个程序满足其行为的正式规范。形式验证的子领域包括演绎验证（见上文）、抽象解释、自动定理证明、类型系统和轻量级形式方法。一种有前景的基于类型的验证方法是依赖类型编程，其中函数的类型包括（至少部分）函数的规范，并且类型检查代码根据这些规范建立其正确性。全功能独立类型语言作为一种特殊情况支持演绎验证。

另一种互补的方法是程序推导，其中通过一系列保持正确性的步骤从功能规范中产生有效的代码。这种方法的一个例子是伯德-梅尔滕斯形式主义，这种方法可以被看作是另一种通过构造实现正确性的形式。

这些技术可以是完备的，这意味着验证的属性可以从语义中逻辑推导出来，或者是不完备的，这意味着没有这样的保证。完备的术只有在搜索了整个可能性空间后才会产生结果。不完备技术的一个例子是只搜索可能性的一个子集，例如只搜索不超过一定数量的整数，并给出“足够好”的结果。技术也可以是可判定的，这意味着它们的算法实现保证以一个答案结束，或者是不可判定的，这意味着它们可能永远不会结束。因为它们是有界的，不完备的技术往往比完备的技术更容易判定的。

2 检验和确认编辑

验证是测试产品适用性的一个方面。检验互补的方面。人们通常把整个检查过程称为验证和确认（V&V）。

  • 验证：“我们在努力做正确的事情吗？”即产品是否符合用户的实际需求？
  • 确认：“我们做了我们想要做的吗？”，即产品是否符合规格？

验证过程包括静态/结构和动态/行为方面。例如，对于软件产品，可以检查源代码（静态）并针对特定的测试用例（动态）运行。确认常只能动态完成，即产品通过典型和非典型使用进行测试（“它是否令人满意地满足所有用例？”）。

3 自动化程序修复编辑

程序修复是相对于预言机执行的，包括用于验证生成的修复的程序的所需功能。一个简单的例子是测试套件——输入/输出对指定了程序的功能。使用了多种技术，最显著的是使用可满足性模理论解算器，[4]和使用进化计算的遗传编程，[5] 来生成和评估修复的可能方法。前者是确定性的，而后者是随机的。

程序修复结合了形式验证和程序综合技术。形式验证中的故障定位技术用于计算程序点，这些程序点可能是可能的错误位置，可以被综合模块作为目标。为了减少搜索空间，修复系统通常集中在一个小的预定义的bug类上。工业应用受到现有技术计算成本的限制。

4 工业用途编辑

设计复杂性的增长提升了形式验证技术在硬件行业中的重要性。[6][7]目前，大多数或所有领先的硬件公司都在使用形式验证，[8] 但它在软件业的应用仍在萎靡不振。这可归因于硬件行业的更大需求，在硬件行业，错误具有更大的商业意义。由于组件之间潜在的微妙相互作用，通过仿真模拟现实变得越来越困难。硬件设计的重要方面可以采用自动化的验证方法，使得正式的验证更容易引入，也更有效率。[9]

截至2011年，已正式验证了几个操作系统：NICTA的安全嵌入式L4微内核，由OK Labs以seL4的形式进行商业销售；[10] 华东师范大学基于OSEK/VDX的实时操作系统；Green Hill Software 开发的的完整性操作系统；和SYSGO的PikeOS。[11][12]

截至2017年，形式验证已通过网络数学模型应用于大型计算机网络的设计，[13] [14] 并作为新网络技术类别（基于意图的网络）的一部分。[15] 提供形式验证解决方案的网络软件供应商包括思科（Cisco）[16] 转发网络（Forward Networks）[17][18] 和Veriflow系统（Veriflow Systems）。[19]

计算机证书编译器是一个形式验证的编译器，实现了国际标准化组织的大部分内容。

参考文献

  • [1]

    ^Sanghavi, Alok (May 21, 2010). "What is formal verification?". EE Times Asia..

  • [2]

    ^Introduction to Formal Verification, Berkeley University of California, Retrieved November 6, 2013.

  • [3]

    ^Cohen, Ben; Venkataramanan, Srinivasan; Kumari, Ajeetha; Piper, Lisa (2015). SystemVerilog Assertions Handbook (4th ed.). CreateSpace Independent Publishing Platform. ISBN 978-1518681448..

  • [4]

    ^Favio DeMarco; Jifeng Xuan; Daniel Le Berre; Martin Monperrus (2014). Automatic Repair of Buggy If Conditions and Missing Preconditions with SMT. Proceedings of the 6th International Workshop on Constraints in Software Testing, Verification, and Analysis (CSTVA 2014). pp. 30–39. arXiv:1404.3186. doi:10.1145/2593735.2593740. ISBN 9781450328470..

  • [5]

    ^Le Goues, Claire; Nguyen, ThanhVu; Forrest, Stephanie; Weimer, Westley (January 2012). "GenProg: A Generic Method for Automatic Software Repair". IEEE Transactions on Software Engineering. 38 (1): 54–72. doi:10.1109/TSE.2011.104..

  • [6]

    ^Harrison, J. (2003). "Formal verification at Intel". 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings. pp. 45–54. doi:10.1109/LICS.2003.1210044. ISBN 978-0-7695-1884-8..

  • [7]

    ^Formal verification of a real-time hardware design. Portal.acm.org (June 27, 1983). Retrieved on April 30, 2011..

  • [8]

    ^"Formal Verification: An Essential Tool for Modern VLSI Design by Erik Seligman, Tom Schubert, and M V Achutha Kirankumar". 2015..

  • [9]

    ^"Formal Verification in Industry" (PDF). Retrieved September 20, 2012..

  • [10]

    ^"Abstract Formal Specification of the seL4/ARMv6 API" (PDF). Archived from the original (PDF) on May 21, 2015. Retrieved May 19, 2015..

  • [11]

    ^Christoph Baumann, Bernhard Beckert, Holger Blasum, and Thorsten Bormer Ingredients of Operating System Correctness? Lessons Learned in the Formal Verification of PikeOS.

  • [12]

    ^"Getting it Right" by Jack Ganssle.

  • [13]

    ^Heller, Brandon. "Seeking truth in networking: from testing to verification". Forward Networks. Retrieved February 12, 2018..

  • [14]

    ^Scroxton, Alex. "For Cisco, intent-based networking heralds future tech demands". Computer Weekly. Retrieved February 12, 2018..

  • [15]

    ^Lerner, Andrew. "Intent-based networking". Gartner. Retrieved February 12, 2018..

  • [16]

    ^Kerravala, Zeus. "Cisco brings intent based networks to the data center". NetworkWorld. Retrieved February 12, 2018..

  • [17]

    ^""Forward Networks: Accelerating and De-risking Network Operations". Insights Success. Retrieved February 12, 2018..

  • [18]

    ^"Getting Grounded in Intent=based Networking" (PDF). NetworkWorld. Retrieved February 12, 2018..

  • [19]

    ^"Veriflow Systems". Bloomberg. Retrieved February 12, 2018..

阅读 78
版本记录

  • 暂无