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

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
participants (1)
-
Frank Dedden