From Fedora Project Wiki


The Copilot Runtime Verification Framework

Summary

Copilot Language and Runtime Verification System is a stream-based runtime-verification framework for generating hard real-time C code.


Owner

Current status

Detailed Description

Copilot is a realtime programming language and Runtime Verification framework, developed for NASA. It allows users to write concise programs in a simple but powerful way using a stream-based approach.

Programs can be interpreted for testing, or translated C99 code to be incorporated in a project, or as a standalone application. The C99 backend ensures us that the output is constant in memory and time, making it suitable for systems with hard realtime requirements.

Feedback

Benefit to Fedora

This is a new feature in Fedora which will of interest to those developing specific critical embedded systems requiring a high level of software assurance.


Scope

  • Proposal owners:
    • build the copilot stack for Rawhide/F42: version 3.19 is packaged [done]
  • Other developers:
  • Policies and guidelines: N/A (not needed for this Change)
  • Trademark approval: N/A (not needed for this Change)
  • Alignment with the Fedora Strategy:

Upgrade/compatibility impact

Early Testing (Optional)

Do you require 'QA Blueprint' support? Y/N

How To Test

  • sudo dnf install ghc-copilot-devel
  • follow the documentation below for tutorial examples


User Experience

Users will be able to easily install the Copilot verification framework and test it.

Dependencies

Contingency Plan

  • Contingency mechanism: (What to do? Who will do it?) N/A (not a System Wide Change)
  • Contingency deadline: N/A (not a System Wide Change)
  • Blocks release? N/A (not a System Wide Change), Yes/No


Documentation

Release Notes

Retrieved from "https://fedoraproject.org/w/index.php?title=Changes/Copilot_Runtime_Verification_Framework&oldid=733686"