Applying Formal Methods Tools to an Electronic Warfare Codebase (Experience report)

TL;DR

This paper reports on applying formal methods tools to an electronic warfare system, highlighting usability challenges, differences from unit testing, and proposing improvements based on practical experience.

Contribution

It provides practical insights into integrating formal methods into industrial EW software, emphasizing usability barriers and suggesting enhancements for better adoption.

Findings

Formal methods tools detect different vulnerabilities.

Usability issues hinder widespread adoption.

Recommendations include better documentation and automation.

Abstract

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.