正式方法

在计算机科学中，正式方法是数学上严格的技术，用于软件和硬件系统的规范，开发，分析和验证。将正式方法用于软件和硬件设计的动机是由于在其他工程学科中，进行适当的数学分析可以有助于设计的可靠性和鲁棒性。

正式方法采用各种理论计算机科学基础知识，包括逻辑计算，形式语言，自动机理论，控制理论，程序语义，类型系统和类型理论。

背景

半正式方法是形式主义和语言，这些语言和语言不被认为是完全“正式”的。它违背了将语义完成到以后阶段的任务，然后通过人类的解释或通过诸如代码或测试用例生成器之类的软件来完成。

分类

正式方法可以在多个级别使用：

0级：可以进行正式规范，然后非正式地从该计划制定。这被称为正式方法。在许多情况下，这可能是最具成本效益的选择。
1级：正式的开发和正式验证可用于以更正式的方式制定程序。例如，可以进行财产的证明或从规范到程序的改进。这可能是涉及安全或保障的高融合系统中最合适的。
第2级：定理抛弃可以用于进行全正式的机器检查证明。尽管工具提高和成本下降，但这可能非常昂贵，并且只有在错误成本很高的情况下（例如，在操作系统或微处理器设计的关键部分）时，实际上才值得。

有关此信息的更多信息将在下面扩展。

与编程语言语义一样，形式方法的样式可能大致分类如下：

语义语义，其中系统的含义在域的数学理论中表达。这种方法的支持者依赖于领域的众所周知的本质来赋予系统意义。评论家指出，并非每个系统都可以直观或自然地视为功能。
操作语义，其中系统的含义表示为（可能是）简单的计算模型的一系列动作。这种方法的支持者指出，其模型的简单性是表达清晰度的一种手段。批评家反驳说，语义问题刚刚被延迟（谁定义了更简单的模型的语义？）。
公理语义，其中系统的含义是根据系统在系统之前和之后执行任务的前提条件和后条件来表达的。支持者注意到与经典逻辑的联系；批评家指出，这种语义从未真正描述系统的作用（仅仅是之前和之后的真实）。

轻巧的形式方法

一些从业者认为，正式的方法社区已经过分强调了规范或设计的正式化。他们认为，所涉及的语言的表现力以及所建模的系统的复杂性，使充分的形式化成为困难且昂贵的任务。作为替代方案，已经提出了各种轻巧的正式方法，强调部分规范和集中应用。这种对形式方法的轻巧方法的示例包括合金对象建模符号，丹尼与用例驱动开发的Z符号某些方面的合成以及CSK VDM工具。

用途

正式方法可以通过开发过程在各个点应用。

规格

正式的方法可用于对要开发的系统的描述，无论是所需的细节级别。该正式描述可用于指导进一步的开发活动（请参阅以下各节）；此外，它可以用来验证开发系统的要求已被完全准确地指定，或者通过以精确且明确定义的语法和语义来表达正式语言来形式化系统要求。

多年来，人们已经注意到了正式规格系统的需求。在Algol 58报告中， John Backus提出了描述编程语言语法的正式符号，后来命名为Backus正常形式，然后更名为Backus -Naur表格（BNF）。 Backus还写道，对句法有效Algol程序含义的正式描述尚未及时完成报告。 “因此，对法律计划的语义的正式处理将包括在随后的论文中。”它从未出现过。

发展

形式开发是将形式方法用作工具支持的系统开发过程的集成部分。

一旦制定了正式规范，该规范可以用作指南，同时在设计过程中开发混凝土系统（即通常在软件中实现，但也有可能在硬件中实现）。例如：

如果形式规范在操作语义中，则可以将观察到的混凝土系统行为与规范的行为进行比较（本身应该是可执行的或可模拟的）。此外，规范的操作命令可以正常地将转换转换为可执行代码。
如果形式规范是在公理语义中，则规范的前提条件和后条件可能会成为可执行代码中的主张。

确认

正式验证是使用软件工具来证明正式规范的属性，或者证明系统实施的形式模型满足其规范。

一旦开发了形式规范，该规范就可以用作证明规范属性的基础，并通过推断系统实施的属性。

签名验证

登录验证是使用高度信任的正式验证工具的使用。这样的工具可以替代传统的验证方法（甚至可以认证该工具）。

以人为导向的证据

有时，证明系统正确性的动机并不是要保证系统正确性的明显需求，而是更好地理解系统的愿望。因此，使用自然语言的数学证明风格（或排便），使用此类证明的一定程度的非正式性来制作一些正确性的证明：使用自然语言的手写（或排版）。 “好”证明是其他人类读者可以阅读和可理解的证据。

对这种方法的批评者指出，自然语言固有的歧义允许在这种证据中未发现错误。通常，在低级细节中可能会出现微妙的错误，通常会被这些证据所忽略。此外，产生这样的良好证据所涉及的工作需要高水平的数学成熟和专业知识。

自动证明

相比之下，通过自动手段产生此类系统正确性的证据，人们越来越兴趣。自动化技术分为三个一般类别：

自动化定理证明了系统试图从头开始产生正式的证据，给定对系统的描述，一组逻辑公理和一组推理规则。
模型检查，其中系统通过详尽的搜索系统可以在执行过程中输入的所有可能状态来验证某些属性。
抽象的解释，其中系统使用（可能是完整的）代表它的晶格验证了程序的行为属性过度透明度。

一些自动化的定理掠夺需要指导哪些属性“有趣”以追求，而另一些则在没有人类干预的情况下工作。如果没有给出足够的抽像模型，则模型检查器可能会很快陷入检查数百万个无趣的状态时。

这种系统的支持者认为，由于所有乏味的细节均已验证，因此结果比人类制作的证明具有更大的数学确定性。使用此类系统所需的培训也小于手工产生良好数学证明所需的培训，这使得多种从业者可以使用这些技术。

批评家指出，其中一些系统就像口腔：它们发表了真理的声明，但没有对真理的解释。还有“验证验证者”的问题；如果有助于验证的程序本身未经证实，则可能有理由怀疑产生的结果的合理性。一些现代模型检查工具产生了“证明日志”，详细介绍了他们的证明中的每个步骤，从而可以执行适当的工具，独立验证。

抽象解释方法的主要特征是它提供了合理的分析，即没有返回错误的负面因素。此外，通过调整代表要分析的属性的抽象域，并应用加宽的操作员以获得快速收敛，它是有效扩展的。

申请

正式方法应用于硬件和软件的不同领域，包括路由器，以太网交换机，路由协议，安全应用程序和操作系统的微动力器，例如SEL4 。有几个示例已被用来验证数据中心中使用的硬件和软件的功能。 IBM在AMD X86处理器开发过程中使用了ACL2 ，一种定理供体。英特尔使用此类方法来验证其硬件和固件（已编程为只读内存的永久软件）。 Dansk Datamatik中心在1980年代使用了正式方法来开发ADA编程语言的编译器系统，该系统随着长期寿命的商业产品。

NASA还有其他一些应用正式方法的项目，例如下一代航空运输系统，国家空域系统中的无人飞机系统集成以及空中协调的冲突解决和检测（ACCORD）。 B-Method带有Atelier B ，用于为Alstom和Siemens在世界范围内安装的各种地铁以及常见的标准认证以及Atmel和Stmicroelectronics对系统模型的开发开发安全自动化。

大多数知名的硬件供应商（例如IBM， Intel和AMD）经常在硬件中使用正式验证。硬件有许多领域，英特尔使用正式方法来验证产品的工作，例如，CACHE-COHERENT协议的参数化验证，Intel Core i7处理器执行引擎验证（使用定理证明， BDD和符号评估），使用HOL Light Theorem Prover对Intel IA-64体系结构进行优化，以及对PCI Express协议和使用Cadence的Intel Advance Management技术的支持高性能双端口千兆以太网控制器的验证。同样，IBM在验证电源门，寄存器和IBM Power7微处理器的功能验证时使用了形式方法。

在软件开发中

在软件开发中，正式方法是在需求，规范和设计级别上解决软件（和硬件）问题的数学方法。正式方法最有可能应用于安全至关重要的软件和系统（例如航空电子软件）。软件安全保证标准（例如DO-178C）允许通过补充来使用正式方法，常见标准要求最高分类的正式方法。

对于顺序软件，形式方法的示例包括B-Method ，自动定理中使用的规范语言证明，提升和Z符号。

在功能编程中，基于属性的测试允许对单个功能的预期行为进行数学规范和测试（如果不是详尽的测试）。

对象约束语言（以及Java建模语言）允许正式指定面向对象的系统，即使不一定正式验证。

对于并发软件和系统，培养皿网，过程代数和有限状态机器（基于自动机理论；另请参见虚拟有限状态机或事件驱动的有限状态机器）允许可执行的软件规范，可用于构建和验证应用行为。

软件开发中形式方法的另一种方法是用某种形式的逻辑编写规范（通常是一阶逻辑的变化），然后直接执行逻辑，就好像它是一个程序一样。基于描述逻辑的 OWL语言就是一个示例。还可以自动从逻辑上自动映射某些版本的英语（或其他自然语言），并直接执行逻辑。示例是尝试控制的英语和互联网业务逻辑，这些逻辑不寻求控制词汇或语法。支持双向英语绘制映射和直接执行逻辑的系统的一个功能是，它们可以在商业或科学层面上以英语或科学层面来解释其结果。

正式的方法和符号

有多种形式的方法和符号可用。

规范语言

模特检查器

ESBMC
MALPAS软件静态分析工具集- 用于正式安全 - 关键系统证明的工业强度模型检查器
PAT - 并发系统和CSP扩展程序的免费模型检查器，模拟器和精炼检查器（例如，共享变量，数组，公平性）
旋转
Uppaal

解决者和比赛

正式方法中的许多问题都是NP-HARD ，但在实践中产生的情况下可以解决。例如，布尔值的令人满意的问题是Cook-Levin定理的NP完整问题，但是SAT求解器可以解决各种大型实例。有一些“解决者”出于正式方法中出现的各种问题，并且有许多定期竞争可以评估解决此类问题的最新问题。

SAT比赛是每年一次的比赛，可以比较SAT求解器。 SAT求解器用于合金等形式方法工具。
CASC是年度自动定理掠夺者的年度竞赛。
SMT-COMP是SMT求解器的年度竞争，可用于正式验证。
CHC-COMP是每年通过受约束的Horn条款的求解器的竞争，这些求解器具有正式验证的应用。
QBFEVAL是针对真实量化布尔公式的求解器的每两年一次的竞争，它们具有用于模型检查的应用。
SV-COMP是软件验证工具的年度竞赛。
Sygus-Comp是计划合成工具的年度竞争。