Copilot

A stream DSL for writing embedded C programs

View My GitHub Profile

Introduction

Copilot is a runtime verification framework written in Haskell. It allows the user to write programs in a simple but powerful way using a stream-based approach.

Programs can be interpreted for testing, or translated C99 code to be incorporated in a project, or as a standalone application. The C99 backend ensures us that the output is constant in memory and time, making it suitable for systems with hard realtime requirements.

Installation

Currently the Copilot 3.0 release requires GHC 8.0 or higher.

Copilot is available from Hackage, and the latest version can be installed easily:

cabal install copilot

Alternatively one can download and install it from the repositories as well:

git clone --recursive https://github.com/Copilot-Language/Copilot.git
cd Copilot
git submodule update --init --remote
make

Typically one would only go this route to develop Copilot. For regular users the cabal method is highly recommended.

Example

Here follows a simple example of a heating system. Other examples can be found in the Examples directory of the main repository.

-- This is a simple example with basic usage. It implements a simple home
-- heating system: It heats when temp gets too low, and stops when it is high
-- enough. It read temperature as a byte (range -50C to 100C) and translates
-- this to Celcius.

module Heater where

import Language.Copilot
import Copilot.Compile.C99

import Prelude hiding ((>), (<), div)

-- External temperature as a byte, range of -50C to 100C
temp :: Stream Word8
temp = extern "temperature" Nothing

-- Calculate temperature in Celcius.
-- We need to cast the Word8 to a Float. Note that it is an unsafeCast, as there
-- is no direct relation between Word8 and Float.
ctemp :: Stream Float
ctemp = (unsafeCast temp) * (150.0 / 255.0) - 50.0

spec = do
  -- Triggers that fire when the ctemp is too low or too high,
  -- pass the current ctemp as an argument.
  trigger "heaton"  (ctemp < 18.0) [arg ctemp]
  trigger "heatoff" (ctemp > 21.0) [arg ctemp]

-- Compile the spec
main = reify spec >>= compile "heater"

Documentation

A manual to Copilot can be downloaded here.

Copilot comes with a set of examples as part of its distribution, available in the Examples directory of the main repository.

Structure and Sources

Apart from the Copilot Github project page, there are a number of sub-projects that make up Copilot:

Additionally there is a specific repository that lists most of the papers and articles written on Copilot: copilot-discussion.

Acknowledgements

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!

License

Copilot is distributed under the BSD-3-Clause license, which can be found here

Issues / Bugs

If you happen to find any issues or bugs, please add an issue to the corresponding repository on our Github pages.

Contact

The project is currently maintained by Frank Dedden and Alwyn Goodloe (NASA Langley Research Center). For any questions, remarks, ideas etc. please send an email to dev@dedden.net.

The Copilot Team

The development of Copilot spans across several years. During these years the following people have helped develop Copilot (in no particular order):