Copilot is a Haskel DSL for defining software health monitors in embedded systems.
It uses other DSLs called Atom and SBV for generating C code and verification.
At the highest level a spec defined an set of infinite data streams, the operations to perform on the streams, conditions to monitor the streams for, and functions to call when those conditions occur.
The main data type is Stream, where Stream is an infinite list. You need to specifiy the type of the element so a valid declaration is:
myFirstStream :: Stream Int
Copilot overloads the ++ operator to lift operands to type Stream.
myStream :: Stream Int
myStream = [0,1,2] ++ myStream -- yields [0,1,2] repeating
You can also use drop on Streams.
drop 1 myStream -- yields [1,2] ++ [0,1,2] repeating
Every Copilot program has a spec defining what condition to monitor and what to do when that condition occurs. The action to take when the condition occurs is called the trigger. The spec from the Copilot paper:
propTempRiseShutOff :: Spec
propTempRiseShutOff = do
observer "drop 2 temps" (drop 2 temps)
observer "temps" (temps)
trigger "over_temp_rise"
(overTempRise && running) []
where
-- continues ...
An observer is used for debugging. When you interpret the spec the value of the observed value will be printed for each time step. The form is:
observer "description" (variable_name)
Where description can be an string. It's just the name of the column in the interpreter output.
And trigger has the form:
trigger "functionname" (Stream Bool) [arguments]
The functionname function can be a Haskell function or an external C function. The Stream Bool part is the condition to be monitored. The [arguments] get passed to functionname when the trigger fires.
Everything after where are the variables used in the spec. Typically the spec defines its own Streams and extern Streams. The purpose of extern is to model data coming into the monitor from other parts of the system. The code generating the extern Streams can be external C functions.
In this example the Stream representing the data input is called temps:
max = 500 -- maximum engine temperature
temps :: Stream Float
temps = [max, max, max] ++ temp
temp = extern "temp" (Just tempin)
tempin = 100.0:100.0:100.0:repeat 103.0 -- this could be an extern C function
The reason temps has max 3 times at the beginning is just to give it an initial value. It'll make sense once you see how the condition Stream is defined.
The Stream that represents the condition to be monitored is called overTempRise:
overTempRise :: Stream Bool
overTempRise = drop 2 temps > (2.3 + temps)
In the example, we only want the monitor to run when the engine is running, so another Stream is defined as running:
running :: Stream Bool
running = extern "running" (Just (repeat True))
Here, running is always True but it could be something more exciting.
The complete program is:
import Language.Copilot
import qualified Prelude as P
propTempRiseShutOff :: Spec
propTempRiseShutOff = do
observer "drop 2 temps" (drop 2 temps)
observer "temps" (temps)
trigger "over_temp_rise"
(overTempRise && running) []
where
max = 500 -- maximum engine temperature
temps :: Stream Float
temps = [max, max, max] ++ temp
temp = extern "temp" (Just tempin)
tempin = 100.0:100.0:100.0:repeat 103.0
overTempRise :: Stream Bool
overTempRise = drop 2 temps > (2.3 + temps)
running :: Stream Bool
running = extern "running" (Just (repeat True))
To interpret (simulate) the spec start ghci, load the module and type:
interpret 10 propTempRiseShutOff
The output is:
over_temp_rise: drop 2 temps: temps:
-- 500.0 500.0
-- 100.0 500.0
-- 100.0 500.0
-- 100.0 100.0
() 103.0 100.0
() 103.0 100.0
-- 103.0 103.0
-- 103.0 103.0
-- 103.0 103.0
-- 103.0 103.0
The () indicate when the trigger fired. This occurs when drop 2 temps is greater than 2.3 + temps. The "current" temperature value for this tick is drop 2 temps and the temperature value 2 ticks ago is temps. One item is dropped from the infinite Stream each tick.