An Assured Open-Source Framework for Runtime Verification

The Copilot Runtime Verification Framework transforms high-level specifications written in a variety of specification languages into efficient runtime monitors. Developed as a collaborative effort among NASA (Langley and Ames), Galois, and the National Institute of Aerospace, Copilot is targeted at safety-critical hard real-time systems and served as an experimental platform enabling a research program in highassurance runtime verification. Successful use in controlled experiments culminated in a desire to use it in critical flight settings. We will describe how what began as research software evolved into an open source NASA Class D Software Engineering tool, where we are able to certify the generated monitors as safetycritical flight software. To get there, our software development processes had to migrate from "how we did it in graduate school" to following prescribed NASA software engineering standards (NPR 7150.2). Moreover, we will discuss how state-of-the-art approaches to software testing, as well as automated formal verification, are applied to assure that a very complex software artifact is correct. In addition, we will present our processes for handling open source contributions.

Alwyn E. Goodloe, NASA Langley Research Center.

Ivan Perez, NASA Ames Research Center/KBR

Ryan Scott, Galois Inc.