Runtime Verification in Real-Time with the Copilot Language: A Tutorial

摘要

Abstract Ultra-critical systems require high-level assurance, which cannot always be guaranteed at compile time. The use of runtime verification (RV) enables monitoring of these systems during runtime, to detect illegal states early and limit their potential consequences. This paper is a tutorial on RV using Copilot, an open-source runtime verification framework actively used by NASA to carry out experiments with robots and unmanned aerial vehicles. Copilot monitors are written in a compositional, stream-based language, which the framework automatically translates into real-time C code that satisfies static memory requirements suitable to run on embedded hardware. Copilot includes multiple libraries that extend the core functionality with higher-level constructs, Boyer-Moore majority voting, and a variety of Temporal Logics (TL), resulting in robust, high-level specifications that are easier to understand than their traditional counterparts.