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.
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.
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"
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.
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.
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!
Copilot is distributed under the BSD-3-Clause license, which can be found here
If you happen to find any issues or bugs, please add an issue to the corresponding repository on our Github pages.
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 firstname.lastname@example.org.
The development of Copilot spans across several years. During these years the following people have helped develop Copilot (in no particular order):