Hi everyone!!
We are very excited to announce Copilot 3.17 [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.
Copilotis being 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 release introduces compatibility with what4 versions up to 1.5.1, and replaces several functions in copilot-core. The second change is a breaking change: the functions replaced have been deprecated and new alternatives introduced instead.
As always, we're releasing exactly 2 months since the last release. Our next release is scheduled for Jan 7th, 2024.
In
our last announcement, we mentioned 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-libraries 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
[1] https://github.com/nasa/ogma
[2] https://github.com/Copilot-Language/copilot/releases/tag/v3.17