[Haskell-cafe] [Announcement] Copilot 3.0, a hard realtime C generator and runtime verification framework
frank at dedden.net
Tue Apr 9 15:23:42 UTC 2019
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
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
* 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 . For more information, including
documentation, examples and links to the source code, please visit the webpage
The Copilot developers:
- Frank Dedden (maintainer)
- Alwyn Goodloe (maintainer)
- Ivan Perez
More information about the Haskell-Cafe