Look What You Made Me Do: Formal Methods and the Verification-Validation Gap in System Assurance

Research in formal methods for engineering reliable autonomous systems has focused almost exclusively on verifying that system behavior meets specifications. While these endeavors have yielded important contributions and even mathematical guarantees, the field’s focus has generally left open the question of whether systems that use formal methods can be well-validated, that is, whether the specifications can be appropriately checked against the intent of stakeholders. It is no use to guarantee that a system meets specification if the specification as written is not actually what the user wanted.In this work, we highlight issues arising from this lack of consideration and their impacts in real-world systems. We then consider the various levers that are available to us when designing abstractions of specifications for the validation task, and how those may be matched to different stakeholders and their needs through the lens of situation awareness. Finally, we highlight developments in the formal methods space that may lend themselves to improvements in validation of systems utilizing formal methods.