[ANN] Copilot 3.14 - Runtime Verification Haskell EDSL used at NASA

Hi everyone,

I’m very excited to announce Copilot 3.14. Copilot is a stream-based EDSL in Haskell for writing and monitoring embedded C programs, with an emphasis on correctness and hard realtime requirements. Copilot is typically used as a high-level runtime verification framework, and supports temporal logic (LTL, PTLTL and MTL), clocks and voting algorithms.

Among others, Copilot has been used at the Safety Critical Avionics Systems Branch of NASA Langley Research Center for monitoring test flights of drones. Through the NASA tool Ogma (GitHub - nasa/ogma), which is also written in Haskell, Copilot also serves as a runtime monitoring backend for the requirements elicitation tool FRET, and can target NASA’s Core Flight System and the Robot Operating System (ROS2) applications.

This new version provides up-to-date compiler support, simplifies the API, and improves the documentation. As always, we’ve released exactly on schedule (2 months since the last release).

For details, see: GitHub - Copilot-Language/copilot: A stream-based runtime-verification framework for generating hard real-time C code.

Our next release is scheduled for May 7th, 2023. We have almost completed the C99 unit tests, and plan to include those in the next version. Copilot is currently undergoing the qualification process necessary for NASA Class D Software. Current emphasis is on increasing test coverage, removing unnecessary dependencies, hiding internal definitions, and formatting the code to meet our new coding standards. Users are encouraged to participate by opening issues and asking questions via our github repo.

There’s been A LOT MORE updates on the Copilot front in the last few months. We’ll be able to announce more soon. Stay tuned :radio:

Happy Haskelling!

Ivan

14 Likes

Exciting to see Copilot continue to grow in reach and use!

3 Likes

Congrats on hitting a round number version (8

4 Likes

Hahah that’s a good one

1 Like