From Fedora Project Wiki
Comments and Explanations
The page source contains comments providing guidance to fill out each section. They are invisible when viewing this page. To read it, choose the "view source" link.
Copy the source to a new page before making changes! DO NOT EDIT THIS TEMPLATE FOR YOUR CHANGE PROPOSAL.
Guidance
For details on how to fill out this form, see the documentation.
Report issues
To report an issue with this template, file an issue in the pgm_docs repo.


The Copilot Runtime Verification Framework

This is a proposed Change for Fedora Linux.
This document represents a proposed Change. As part of the Changes process, proposals are publicly announced in order to receive community feedback. This proposal will only be implemented if approved by the Fedora Engineering Steering Committee.

Summary

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


Owner

Current status

  • Targeted release: Fedora Linux 42
  • Last updated: 2025-02-11
  • [Announced]
  • [<will be assigned by the Wrangler> Discussion thread]
  • FESCo issue: <will be assigned by the Wrangler>
  • Tracker bug: <will be assigned by the Wrangler>
  • Release notes tracker: <will be assigned by the Wrangler>

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=730697"