[Haskell-cafe] [ANN] Copilot 3.11 -- hard realtime C runtime verification

Ivan Perez ivanperezdominguez at gmail.com
Thu Sep 8 00:59:39 UTC 2022


Dear all,

We are very happy to announce the release of Copilot 3.11. Copilot is a
runtime verification system implemented as a Haskell DSL that generates
hard-realtime C99. Among others, Copilot is being used by the Safety
Critical Avionics Systems Branch of NASA Langley Research Center for
monitoring test flights of drones. You can learn more about it at [1].

Copilot 3.11 introduces a new library, copilot-interpreter, that
isolates all functions related to simulation of Copilot specifications.
The release also contains a number of bug fixes, provides a simplified
API, deprecates outdated elements, removes unused code, and introduces
support for GHC 9.2. A full list of changes merged is available at [2].

A substantial effort is being made to achieve NASA's Class D software
classification, most notably in terms of development process (which you
can partly witness in how issues and PRs are being handled on our github
repo), test coverage (mostly with quickcheck), and proofs of correctness
of the generated code (with what4).

Copilot is being used by the Safety-Critical Avionics Systems Branch
(D320) of NASA Langley Research Center to conduct experiments related to
flight safety of aerial vehicles. We have also built Ogma [3], a tool
that allows us to generate full monitoring applications (e.g., NASA's
Core Flight System [4] and Robot Operating System [5] applications) from
requirements in structured natural language.

We invite you all to explore Copilot, to try it, and to extend it. If
you like it, please help us draw attention to this work with a star on
github or a mention online.

Happy Haskelling,
The Copilot Team

[1] https://github.com/Copilot-Language/copilot
[2] https://github.com/Copilot-Language/copilot/milestone/15?closed=1
[3] https://github.com/nasa/ogma
[4] https://cfs.gsfc.nasa.gov/
[5] https://www.ros.org/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20220907/8e734a52/attachment.html>


More information about the Haskell-Cafe mailing list