虽然使用形式化方法相较于单元测试具有优势，但其陡峭的学习曲线常令开发人员望而却步，并可能成为广泛采用的主要障碍。为了支持其融入工业软件工程工作流程，工具必须提供有用的信息，且用户需付出的努力相对较小。本文讨论了在安全要求严苛的电子战系统上识别和应用形式化方法工具的相关经验，并呈现了来自精通开发但缺乏形式化方法培训的电子战软件工程师对这类工具的看法。除了形式化方法与单元测试在思维模式上的差异外，一些形式化方法工具使用的术语或注释与其目标编程语言不同，这构成了另一个采用障碍。输入/输出契约、函数影响的内存对象以及循环不变量可能都难以理解和使用。除了可用性，我们的发现还包括对不同工具所检测漏洞的比较。最后，提出了改进形式化方法可用性的建议，包括更好的能力文档、减少手动工作量以及改进对库代码的处理。

形式化方法被定义为在系统开发中使用数学模型[70]。证明为系统在所有可能执行路径上的正确性提供了严格证据，而单元测试仅能展示在特定用例下的正确性。软件缺陷在生产后修复的成本是设计阶段检测到缺陷所需成本的30倍，2022年仅软件补丁在美国就造成了约1.5万亿美元的损失[41]。研究表明，使用形式化方法最终会降低系统开发成本[14]。然而，形式化方法对普通开发人员而言被认为是令人生畏的，尤其是高昂的初始学习成本，甚至专家也认为形式化规约具有难度[29,10,18,34]。在对专家的调查中，业界采用形式化方法的主要障碍包括“工程师缺乏形式化方法的适当培训”、“学术工具有局限性且未得到专业维护”、“形式化方法未正确融入工业设计生命周期”以及“形式化方法学习曲线陡峭”[27]。对此，我们还需补充：形式化方法工具通常文档不一致/不完整，并且工具间术语缺乏统一，导致难以跨工具比较结果。

美国国防高级研究计划局（DARPA）的“PROVERS”项目旨在探索如何将形式化方法工具整合到常规工程开发流程中，供未经高强度培训的普通开发人员使用[3]。我们在该项目中的角色是：1）收集开发人员对不同形式化方法工具的需求和反馈；2）确定如何将这些工具集成到现有的开发工作流程中，在本案例中即一个电子战系统。通过与工程团队讨论并分享各类形式化方法工具，我们收集了关于他们愿意将何种工具纳入其工作流程的反馈。

文中描述了为将其采纳到一个拥有现有代码库的工程项目中而识别形式化方法工具的经验。我们识别了安全需求，调查了可用工具，并确定了那些能解决我们感兴趣的安全问题的工具。第2节描述了我们的系统、从工程师那里收集的需求，并以分类法形式提出了安全需求的概要。第3节描述了可能适用的开源形式化方法工具。第4节描述了我们选择和应用的工具及其用法、能力，以及改进建议。第5节描述了相关工作，第6节对全文进行总结。