NTRS - NASA Technical Reports Server

Back to Results
Copilot 3Ultra-critical systems require high-level assurance, which cannot always be guaranteed in compile time. The use of runtime verification (RV) enables monitoring these systems in runtime, to detect property violations
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
Acquisition Source
Langley Research Center
Document Type
Technical Memorandum (TM)
Ivan Perez ORCID
(National Institute of Aerospace Hampton, Virginia, United States)
Frank Dedden
(National Aerospace Laboratory Amsterdam, Netherlands)
Alwyn Goodloe
(Langley Research Center Hampton, Virginia, United States)
Date Acquired
May 6, 2020
Publication Date
April 1, 2020
Subject Category
Computer Programming And Software
Report/Patent Number
Funding Number(s)
WBS: 340428.
Distribution Limits
Portions of document may include copyright protected material.
No Preview Available