[Haskell-cafe] [Announcement] Copilot 3.0, a hard realtime C generator and runtime verification framework

[Frank Dedden]

Dear all,

We are very pleased to announce the release of Copilot 3.0, a stream-based DSL
for writing and monitoring embedded C programs, with an emphasis on correctness
and hard realtime requirements.

Copilot is typically used as a runtime verification framework, where programs
serve as specifications to the system we want to monitor. Additional libraries
provide utility functions for temporal logic (LTL, PTLTL and MTL), clocks and
voting algorithms.

Over the years, Copilot has been used at the Safety Critical Avionics Systems
Branch of NASA Langley Research Center for monitoring test flights of drones.

This new release contains a number of additional features that make writing
programs easier:

* The extended language with support for monitoring and generating
  structs and arrays in a type-safe manner.

* A completely rewritten C99 code generator to support the new features.

* Significant improvements on the quality and readability of the output code,
  which help in traceability and certification of the code.

* Internal simplifications for a more future proof codebase.

Copilot is available on hackage [1]. For more information, including
documentation, examples and links to the source code, please visit the webpage
[2].

Kind regards,
The Copilot developers:
- Frank Dedden (maintainer)
- Alwyn Goodloe (maintainer)
- Ivan Perez

[1] http://hackage.haskell.org/package/copilot
[2] https://copilot-language.github.io