Campus Units

Aerospace Engineering, Electrical and Computer Engineering

Document Type

Conference Proceeding

Conference

Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2016)

Publication Version

Accepted Manuscript

Link to Published Version

https://doi.org/10.1007/978-3-319-48869-1_2

Publication Date

2016

Journal or Book Title

Lecture Notes in Computer Science

Volume

9971

First Page

8

Last Page

26

DOI

10.1007/978-3-319-48869-1_2

Conference Date

July 17-18, 2016

City

Toronto, ON, Canada

Abstract

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.

Comments

The final publication is available at Springer via https://doi.org/10.1007/978-3-319-48869-1_2. 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. Posted with permission.

Copyright Owner

Springer International Publishing AG

Language

en

File Format

application/pdf

Published Version

Share

Article Location

 
COinS