Specification: The Biggest Bottleneck in Formal Methods and Autonomy

Supplemental Files
Rozier, Kristin
Journal Title
Journal ISSN
Volume Title
Research Projects
Organizational Units
Aerospace Engineering
Organizational Unit
Computer Science
Organizational Unit
Journal Issue

Advancement of AI-enhanced control in autonomous systems stands on the shoulders of formal methods, which make possible the rigorous safety analysis autonomous systems require. An aircraft cannot operate autonomously unless it has design-time reasoning to ensure correct operation of the autopilot and runtime reasoning to ensure system health management, or the ability to detect and respond to off-nominal situations. Formal methods are highly dependent on the specifications over which they reason; there is no escaping the “garbage in, garbage out” reality. Specification is difficult, unglamorous, and arguably the biggest bottleneck facing verification and validation of aerospace, and other, autonomous systems.

This VSTTE invited talk and paper examines the outlook for the practice of formal specification, and highlights the on-going challenges of specification, from design-time to runtime system health management. We exemplify these challenges for specifications in Linear Temporal Logic (LTL) though the focus is not limited to that specification language. We pose challenge questions for specification that will shape both the future of formal methods, and our ability to more automatically verify and validate autonomous systems of greater variety and scale. We call for further research into LTL Genesis.


This is a post-peer-review, pre-copyedit version of an article published as Rozier K.Y. (2016) "Specification: The Biggest Bottleneck in Formal Methods and Autonomy." In: Blazy S., Chechik M. (eds.) Verified Software. Theories, Tools, and Experiments. VSTTE 2016. Lecture Notes in Computer Science, vol. 9971. The final publication is available at DOI: 10.1007/978-3-319-48869-1_2. Posted with permission.

Model Check, Linear Temporal Logic, Unman Aerial System, Linear Temporal Logic Formula, Sanity Check