early and limit their potential consequences. The introduction of monitors in ultra-critical systems poses a challenge, as failures and delays in the RV subsystem could affect other subsystems and threaten the mission as a whole. This paper presents Copilot 3, a runtime verification framework for real-time embedded systems. Copilot monitors are written in a compositional, stream-based language with support for a variety of Temporal Logics (TL), which results in robust, high-level specifications that are easier to understand than their traditional counterparts. The framework translates monitor specifications into C code with static memory requirements, which can be compiled to run on embedded hardware. This paper presents version 3 of the Copilot language, demonstrates its suitability with a number of examples, and discusses its use in larger applications. Additionally, it describes the framework?s architecture, its implementation as a Domain Specific Language (DSL) embedded in Haskell, and the progress of the project over the years.
Document ID
20200003164
Acquisition Source
Langley Research Center
Document Type
Technical Memorandum (TM)
Authors
Date Acquired
May 6, 2020
Publication Date
April 1, 2020
Subject Category
Report/Patent Number
Funding Number(s)
Distribution Limits
Public
Copyright
Portions of document may include copyright protected material.
No Preview Available