Release 3.12 – 2022-11-07
We are pleased to announce the release of Copilot 3.12, 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 high-level runtime verification framework, and supports temporal logic (LTL, PTLTL and MTL), clocks and voting algorithms.
Among others, Copilot has been used at the Safety Critical Avionics Systems Branch of NASA Langley Research Center for monitoring test flights of drones.
The main changes in this release are as follows:
- A new library
copilot-prettyprinterexposes functions related to the Copilot Core pretty-printing backend. Pre-existing functions included as part of
copilot-coreare now deprecated.
- The C99 backend now produces an additional header file with struct declarations. This file is used by the C implementation file generated by Copilot to define structs before the declarations of the handlers, avoiding potential forward declarations that the C compiler cannot resolve. Users of Copilot can choose to import the same new type declaration header file before the standard Copilot header file in their hand-written code, or use external definitions that declare compatible structs. Note that, in the former case, the header file that declares the structs must be included before the header file that declares the externs, handlers and step function.
- The custom type equality module in
copilot-coreis now deprecated in favor of the definition of type equality in
copilot-theoremnow includes support for proofs by bisimulation necessary for future extensions to Copilot.
copilot-corenow complies with the coding rules established as part of the process of compliance with NASA’s Class D requirements (NPR 7150.2).
This release also continues to use our new software engineering process designed to meet the requirements to obtain NASA’s Class D software classification. Details are available here.
Current emphasis is on improving the codebase in terms of stability and test coverage, 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.
Copilot is distributed under the BSD-3-Clause licence, which can be found here.
We are grateful for NASA Contract NNL08AD13T to Galois, Inc. and the National Institute of Aerospace, which partially supported this work.
Additionally NASA Langley contracts 80LARC17C0004 and NNL09AA00A supported further development of Copilot.
We would like to thank Kaveh Darafsheh (NASA Langley Research Center) for his help with testing Copilot. In addition numerous people have helped with smaller things, reporting bugs etc. Thanks to all of them!