Hi everyone,
We are very excited to announce Copilot 3.16 [2]. 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.
Copilot has been used at NASA in drone test flights. Through the NASA tool Ogma [1] (also written in Haskell), Copilot also serves as a runtime monitoring backend for NASA’s Core Flight System, Robot
Operating System (ROS2), and FPrime (the software framework used in the Mars Helicopter) applications.
This new version provides comprehensive tests for the C99 backend, and introduces a breaking change in the definition of the type Arg in copilot-language. For details, see [2]. The new version is already available on Hackage [4].
As always, we’re releasing exactly 2 months since the last release. Our next release is scheduled for Sep 7th, 2023.
We are also extremely excited to announce that Copilot has received full approval for release as NASA Class D open-source software. Current emphasis is on increasing test coverage for the two remaining libraries without tests (copilot-language and copilot-theorem), 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 [3].
There have been many updates on the Copilot front in the last few months. We’ll be able to announce more soon. Stay tuned.
Happy Haskelling!
Ivan