FSL Sponsor Abstract: U.S. Air Force Office of Scientific Research

Runtime verification (RV) refers to the use of lightweight yet powerful formal techniques to monitor, analyze, and guide the execution of programs at run-time. RV is becoming increasingly important for at least two reasons. First, software systems are becoming more complex and more adaptive, making it difficult to statically understand all of their possible behaviors; this is especially true of mission-critical software on autonomous unmanned vehicles, where completion of mission goals depends upon adaptive responses to changing conditions. RV thus plays a valuable role in helping users monitor and understand system behavior during testing, debugging, and deployment. Second, to increase the reliability of complex adaptive software, RV must monitor and analyze the behavior of the software, its environment, and their interaction, in order to trigger adaptive responses when necessary.

To fill these needs, runtime verification itself must become more flexible and adaptive, and it must be equipped with a recovery framework that will help ensure mission completion in the face of runtime violations. We are developing Adaptive Runtime Verification and Recovery (Arrive), a novel extension of runtime verification in which the runtime verification itself is adaptive. Arrive dynamically allocates more runtime-verification resources to high-criticality monitored objects, thereby increasing the probability of detecting property violations within a given overhead budget. Moreover, when a violation is imminent, Arrive takes adaptive and possibly preemptive action in response, thereby ensuring recovery.

We are investigating three related aspects of Arrive: overhead control, incomplete monitoring, and predictive analysis. We are developing a Simplex architecture for cyber-physical systems by extending Simplex to monitor the software state as well as the physical-plant state. We are evaluating the performance and utility of the Arrive framework through significant case studies, including the runtime monitoring of the command-and-control and energy-management infrastructure of a fleet of UAVs.