While using formal methods offers advantages over unit testing, their steep learning curve can be daunting to developers and can be a major impediment to widespread adoption. To support integration into an industrial software engineering workflow, a tool must provide useful information and must be usable with relatively minimal user effort. In this paper, we discuss our experiences associated with identifying and applying formal methods tools on an electronic warfare (EW) system with stringent safety requirements and present perspectives on formal methods tools from EW software engineers who are proficient in development yet lack formal methods training. In addition to a difference in mindset between formal methods and unit testing approaches, some formal methods tools use terminology or annotations that differ from their target programming language, creating another barrier to adoption. Input/output contracts, objects in memory affected by a function, and loop invariants can be difficult to grasp and use. In addition to usability, our findings include a comparison of vulnerabilities detected by different tools. Finally, we present suggestions for improving formal methods usability including better documentation of capabilities, decreased manual effort, and improved handling of library code.

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