Dear all,
We are very happy to announce the release of Copilot 3.10. Copilot is a
runtime verification system implemented as a Haskell DSL that generates
hard-realtime C99. You can learn more about it at [1].
This new version of Copilot contains a small but important change in how
structs are handled in C functions invoked by the monitors when property
violations are detected. This change is API-breaking, so users of
Copilot may need to adapt their systems accordingly. The release also
contains a number of bug fixes, provides a simplified API, deprecates
outdated elements, removes unused code, and relaxes version constraints
for dependencies. 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] applications) from requirements in structured
natural language.
We'd like to take this opportunity to welcome Will Pogge to the team
with his first commit, and thank the Galois team for their
contributions. We also want to thank everyone who uses and helps promote
Copilot; we are seeing increased attention, and gave three talks in the
last two months at JPL, USC, and VCU, with two more taking place this
month.
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