最近，形式化方法已经在大型工业组织(包括AWS、Facebook/meta和微软)中使用，并已被证明是软件工程过程中发现重要bug的有效部分。也许正因为如此，从业者对更频繁地使用它们感兴趣。然而，正式方法的应用远远少于预期，特别是对于安全关键系统，它们被强烈推荐并具有最大的潜力。我们假设，在这些领域，正式的方法似乎仍然不够适用或准备好了它们的预期用途。在关键软件工程中，当我们谈到形式化方法时，我们指的是什么?从科学和实践的角度来看，这种方法既适用又意味着什么?基于文献中对第一个问题的描述，通过这个宣言，我们确定了关键的挑战，并制定了一套指导原则，当一个正式的方法遵循这些原则时，就会在给定的范围内产生成熟的适用性。该宣言不是对过去的发展进行批评，而是努力促进在任何适当的上下文中增加正式方法的使用，以获得最大的利益。
几十年来，形式方法一直是一个活跃的研究领域。理论基础[1]，方法应用[2,3,4]，以及将[5,6]传授给实践工程师的有效途径[7,8]已经得到了深入的讨论和实证证明。学习这些方法的资源范围从早期的教学大纲[9]到最近的课程材料、脚注1教程论文(例如[10])、工具手册(例如[11])、教科书(例如[12,13])和社区wiki。关于成功的正式方法教学、培训和基于教学的转移的证据正在稳步收集。然而，这些措施的范围还不能保证毕业的软件工程研究人员和实践者有一个稳定的知识和技能基础[14,15]。
在学术界[16,17,18,19,20,21]和工业界[22,23]的专家意见的启发和批评的推动下，形式化方法被认为是为具有关键需求的应用程序开发高度可靠软件的最有前途的工具之一[14]。形式化方法的开发人员一直以在实际环境中的适用性为目标，特别是在不同程度上的成功。事实上，许多实践者相信这些方法的巨大潜力，并将使用它们来获得最大的利益，无论是直接使用还是通过强大的软件工具[15]。尽管在可靠系统和软件的工程实践中应用这些方法有广泛的兴趣，但这一领域尚未成功地采用形式化方法。可以观察到(例如[14,15])，它们的使用仍然明显弱于预期，最令人震惊的是，即使在安全关键领域[24]中，它们的应用部分地通过一系列明确推荐的标准(例如IEC 61508和62443,DO-178)。这一观察的一个渐进例外是铁路领域[25]，其中强烈推荐形式化方法(参见EN 50128和50129)，并经常应用于最高完整性级别的软件。
因此，有理由假设形式方法似乎仍然或再次不够适用或准备好实现其预期目的。另一种解释是，现代编程语言和环境(例如c++ 2017, c#， Go, Java/Scala, Python 3, Rust)隐式地支持20世纪70年代至90年代所谓的形式开发的很大一部分(例如运行时类型检查器，ide中的静态分析，编译器中的内存模型，结构化基本类型(如列表))，并避免了许多难以寻求的错误形式方法最初应该揭示[26]。然而，只有当我们忽略了软件和硬件复杂性的大量增加，以及在具有关键需求的领域中软件使用的增加时，这种解释才是合理的。因此，新的问题和错误出现了，而使用形式化方法的原始理由仍然有效，尽管是在不同的抽象层次上。
从这个角度来看，正式方法的有益使用受到阻碍，例如，由于可扩展性差，工具缺失，不充分或不合格[27]，正式方法的教学和培训没有达到足够的学生和从业者，因此训练有素的人员的缺点[15]。当然，对采用新技术或新方法的自然抵制加剧了这种情况。由于目前缺乏对这些障碍以及正式方法的有效性和生产力的了解[24]，因此对正式方法研究和学术界、监管机构和工业界之间目标导向的合作提出了很高的要求。为了帮助研究和转移工作获得动力并促进成功，我们提出了一些在形成宣言时适用的正式方法的指导原则。
第2节和第3节提供了该宣言的背景和动机，并重点介绍了相关工作。第4节代表宣言，详细强调其十项原则。表1以一种独立的方式总结了宣言。第5节重点介绍了一些正式方法的成功案例。第6节总结了目标，建议了实施宣言的行动，并概述了这些行动的预期影响。第7节警告社会不作为的潜在后果，第8节总结。
从文献中可以得到许多有用的特征。例如，IEEE软件工程知识体系说:“形式化方法是通过应用严格的基于数学的符号和语言来指定、开发和验证软件的软件工程方法”[28，第9-7页，第4.2节]。最近的一个定义[29]很好地涵盖了相关方面，指出“形式化方法是一组基于逻辑、数学和理论计算机科学的技术，用于指定、开发和验证软件和硬件系统。”我们稍微改进一下这个概念，说，通过形式化的方法，我们指的是一个明确的数学模型和关于关键属性的合理逻辑推理[30]——比如可靠性、安全性、可靠性、可靠性、性能、不确定性或成本——一类电气、电子和可编程电子或软件系统。模型检查(参见[31,32])、交互定理证明(例如[33,34,35])、抽象解释和静态分析[36,37,38]、程序验证(例如[39,40,41])和正式契约[42]是通用形式化方法的经典例子。
形式化方法的范围从轻量级到重量级的形式化。前者通常侧重于大规模的完全自动化(例如，模型检查和抽象解释)或向程序员提供正式的技术(例如，通过类型系统、断言语言和IDE集成)。相比之下，后者更侧重于指导软件和系统工程师的手工工作步骤(例如，基于细化的方法，如B[23]、VDM或Z[43])。进一步的方法将几种(正式的)技术结合在构建正确性的哲学下(例如[44])。最后，必须注意的是，在计算机科学的正式基础和在更具体的软件工程领域中通常被理解为正式方法之间存在着自然的重叠。
一般来说，可以将方法看作是指导用户在特定情况下进行下一步操作的分步配方。与其他工程学科类似，形式化方法推动了数学和逻辑在软件工程中的作用
通过在一个领域内一致同意的具有精确含义的符号，使对象明确(如自然过程、信息、人们的思想);
减少对这些对象(例如系统或其功能)的歧义或主观解释，并培养对该领域的精确理解
支持关键或繁琐任务(如分析、验证)的机械化。
这些特征区分了正式和非正式(或“非正式”)方法。形式化方法不仅仅是一种(建模)符号或一种开发或分析方法，它不同于编程语言或软件工程工具。
尽管在正式方法和非正式方法之间没有明确的界限(正式可能在程度上发生)，如果数学和逻辑的使用对于实现一些有用的结果既不是必要的也不是必需的，那么人们可以认为软件工程方法是“非正式的”，并且如果数学或逻辑被用于可靠地实现可靠的结果，那么它就是“正式的”。在基于模型的开发和模型驱动的工程中[45]，非正式、半正式(提供形式化语法)和正式(将形式化语义与此语法相关联)技术之间经常有更细微的区别。
一般来说，“适用的”是指能够在某种确定的和实际相关的范围内应用。更具体地说，应用形式化方法包括在关键系统的设计、开发和分析中使用它，以及它与所使用的系统的实质性集成
开发方法(例如结构化开发、基于模型或模型驱动的工程、基于断言的编程、测试驱动的开发)
规范和建模符号(例如UML, SysML)，特定于领域的语言，或编程语言，以及
工具(例如编译器、检查器、集成开发环境)。
当我们使用术语“适用的”或“适用性”时，我们指的是形式化方法的理想程度或成熟度。因此，这个概念建议进行一些定量的(例如，绩效或经济)评估，以对成熟度水平做出客观的陈述，因此，正式方法的适用性。
例如，具有健全核心的证明助手在逻辑和算法上都是成熟的。但是，如果它的用户界面(例如证明语言和编辑器)或定理开发工具(例如对不变量和证明搜索的帮助)不够先进，它可能就不够适用。
每当我们建议将正式方法作为关键(质量保证)工具用于关键工程任务的核心时，我们都期望其适用性。该任务将主要是一个实际的软件工程任务，但它也可以是计算机科学研究和教学中的工程任务。虽然这种期望可能听起来很明显，但在正式方法研究的背景下就不那么明显了，因为通常没有资金和机会来超越简单的应用程序并走向工业场景。
如果在任务中使用方法的预期收益(例如早期错误减少、设计改进、教学增益、科学洞察力)证明应用它的预期成本(例如形式化工作、时间和资源)是合理的，那么形式化方法就可以说是直接适用的。相反，如果不应用该方法的预期成本(例如，延迟故障处理成本，故障后果)对该任务来说是不合理或不可接受的，则可以说这种方法是间接适用的。
它与其他建模或编程方法、技术或语言的适用性有什么不同?形式化方法要求使用(通过工具和指导)数学结构来表示并使对象(例如软件或系统行为，数据集)的含义简洁。正确地理解和有效地使用这些结构需要特定的抽象能力、要教授的数学技能和持续的面向应用程序的培训。一个适用的形式化方法是在这个特定的上下文中处理这些特定需求的方法。
宣言可以被理解为“关于特定工程任务的一系列技术或专家观点”[46]，社区的“一组承诺”[47]，或者催化社区的“参考焦点”[48]。受到其他领域类似成功努力的启发[48,49]，脚注6我们总结道:宣言表达了一个领域中利益相关者(如专家、思想领袖和用户)之间的一些共识协议，它基于相应的定义，它简明地传达了原则指导，以呼吁的形式披露了目标和承诺，提出了行动建议，可以联合起来，从而发起变革。
摘要
1 介绍
2 背景
3.相关工作
4 宣言及其十项原则
5 正式方法整合和转移的成功案例
6 以影响为导向的行动计划
7 没有宣言的人生
8 有限公司
结论与展望
笔记
参考文献
致谢
作者信息
道德声明
搜索
导航
#####
我们的宣言可以被看作是验证软件计划[50]的具体补充，该计划的长期目标是执行广泛的验证实验和案例研究，改进工具景观，并促进正式方法研究向工业的转移。它还提出了更广泛的数字人文宣言的两个原则:软件研究人员和实践者对他们的技术的影响负责，必须反思他们的方法。
Kapor的宣言[51]提出软件设计是一种不同于软件工程的职业，由用户导向驱动。我们的宣言与Kapor的想法相关，因为它建立在形式化方法对概念原型或设计原型有益的观察之上，形式化的methodists通常处于被忽视的角色，可能类似于20世纪80年代和90年代的软件设计师，并且它提供了形式化methodists为什么以及如何很快成为成功的专业软件设计师的论点。
Ladkin的宣言[46，第10章]包括在实际和符合标准的软件保证中使用形式化方法的原则和步骤。同时，他的宣言涵盖了软件保证的许多领域;关于正式方法指导的部分集中于在保证中使用正式方法。我们的宣言补充了Ladkin的工作，指导准备适用于保证和超越的正式方法。
Rae等人的宣言[47]旨在提高安全科学研究方法的使用，然而，没有触及形式方法在软件安全中的适用性。
本节代表宣言及其目标、原则和目的。每个原则都有更详细的解释和评论。表1载有要传达和参考的宣言的简明版本。
形式化方法的目标是适用性，并已被证明是有效的。由于从业者对更频繁地使用形式化方法感兴趣，因此对它们有明显的需求。然而，形式化方法的应用比预期的要少，特别是在具有关键需求的应用程序领域。
一种临时的诊断是，正式的方法似乎仍然不够适用，也不适合它们的预期用途。因此，我们假设增加它们的适用性将导致在研究和实践中更广泛地采用形式化方法。
表1宣言及其十大原则概览
该宣言推荐了几个原则，当遵循这些原则时，可以证明形式化方法在研究和实际软件工程中的不同程度的适用性。因此，一个适用的正式方法应该实现这些原则的连贯选择，尽管没有期望同时实现所有这些原则是可能的或最佳的。这些原则详细说明如下。
4.2.1 范围
一个正式的方法应该清楚地定义它的适用范围，它的领域特殊性，并提供关于如何在给定范围内应用它的可理解的指导。对有限范围的限制可能会减少正式模型的一些偶然复杂性，从而增加易用性并支持其他原则。脚注9
4.2.2 方法
一个正式的方法应该为方法使用者提供一个循序渐进的配方和程序性的指导，以了解在相应情况下可能采取的后续步骤。例如，它可以支持组合、模块化(例如，使用关于契约[42]的形式推理[52])和细化，并带有各种合理的抽象或简化技术，或者至少是一系列有效的建模和规范指南。
4.2.3 集成
一个正式的方法应该通过与其他方法的整合来创造效益。例如，它可以与
(i)
熟悉设计或工程技术(如基于合同的设计);
(2)
广泛使用的建模技术(例如UML/SysML中使用的状态图);
(3)
一门编程语言(如Javascript, C/ c++， Java)，或
(iv)
过程模型(例如Scrum)。
以这种方式进行集成可以增加有用性和易用性。
4.2.4 Explainability
在成功应用形式化方法后，所证明的内容应该是清晰的[27]。一个最小的要求是，它可以精确地说明哪一个主张已经成立(就像数学定理一样)。更严格的要求是能够生成证书，从而能够独立地检查声明。最后但并非最不重要的是，它要求声明(包括潜在的建模假设)可以传达给人类领域专家，甚至可能传达给最终用户。这种方式的可解释性应该会增加有用性。
4.2.5 自动化
正式的方法应该提供工具支持，以防止用户繁琐的工作步骤，并帮助他们专注于必要的和创造性的步骤。特别是，它应该为应用该方法获得最大收益所需的任何明显或有用的抽象提供自动化支持。自动化通常适用于困难或繁琐的任务，因此可以增加工业规模系统的可伸缩性。
4.2.6 可伸缩性
一种正式的方法应适用于实际有关的比额表，作为该比额表的功能，通过合理的努力加以管理。这一原则很可能通过清晰的方法论(例如，高级算法、抽象、模块化方法)和强大的自动化来促进。
4.2.7 转移
正式的方法应附有教学和培训战略以及相应的材料。脚注12:这种策略和材料可能因一种正式方法而异。然而，普通的研究生和有经验的工程师也应该能够通过合理的努力学习和应用一种方法。值得注意的是，仅仅有好的教材是不足以覆盖足够多的学生和从业人员群体的。
4.2.8 有用性
正式方法的应用应该是有效的。例如，可以证明(例如，使用案例研究或对照实验)如果使用传统或非正式替代方案会有什么不同(例如，比较相对的故障避免或故障检测有效性以及这些指标的经济影响)。可用性作为适用性的主导因素将来自其他原则，例如可解释性。
4.2.9 易用性
正式的方法应该是有效适用的。例如，它可以提供概念、抽象，或者建模和推理原语，帮助具有适当技能(参见培训)的用户在指定的范围内以合理的努力(例如，低抽象工作、低证明复杂性、高生产力)应用它。易用性可以通过其他原则来解决，例如可伸缩性和自动化，但也可以单独处理。有用性和易用性指的是技术接受模型[53]的两个主要结构，技术接受模型是广泛用于评估最终用户信息技术的一类模型。
4.2.10 e估值
上述原则应得到适当的证明。通过显示形式化方法在其指定范围内很好地适用于工程问题和系统的范围，可以令人信服地证明适用性(例如，使用代表性示例，使用其他研究人员或从业者可用的工具，甚至可能使用合格的工具[27])。当一个正式的方法被提议或提出时，应该伴随着关于它的好处和可预见的挑战、限制或障碍的信息。这一原则将科学方法整合到形式方法适用性的论证中。
宣言旨在为正式方法研究的执行、写作和评审提供指导。它可以推动未解决(基准或基本)挑战的选择，并刺激研究提案和项目。此外，它可以促进学术界和工业界之间的进一步互动，并在正式方法开发人员和用户(通过可解释性)和客户(通过经济论证)之间建立联系。
下载原文档：https://link.springer.com/content/pdf/10.1007/s10270-023-01124-2.pdf
