Ultra-critical systems require high level assurance, which cannot always be guaranteed at compile time. The use of runtime verification (RV) allows us to monitor these systems at runtime, detect property violations early, and limit the potential consequences of these errors. Copilot is a stream based high-level EDSL in Haskell to define monitors, it has support for different Temporal Logics (TL), and compiles to hard realtime C99 code specifically suited for embedded systems.

Although simple in its design, and relying on known techniques for EDSL implementation, Copilot is unique due to its domain of application: it is used by NASA researchers to monitor properties of Unmanned Aerial Vehicles for the purposes of verification and validation. The goal of Copilot is to provide a language that is guaranteed to compile to correct C code, targeted at people with minimal knowledge of Haskell.

In this talk we will discuss the internals of Copilot 3.0 and some of the obstacles that currently limits its use. In particular:

• We will explain how support for structs and arrays is implemented, using type-level programming to provide compile-time guarantees and make generation of C code possible.

• We will demonstrate how Copilot generates hard realtime C99, how memory consumption is known in advance, and the constraints that imposes in our EDSL.

Current obstacles, especially for our target audience, include:

• Error messages are harder to understand, in part due to the use of dependent types, as well as due to the way two-stage compilation of EDSL’s is done.

• The current implementation sometimes requires additional boilerplate to be defined by users, especially when they use structs.

Website: https://copilot-language.github.io