Real-time control systems, such as the microcontroller that controls your car's brakes, can have horrific consequences if they go wrong. That's why, for safety-critical software, we need real assurance that the software always does the right thing.
We can write unit tests to check that our software does the right thing in specific situations, but for a control system with a large state that is supposed to run continuously for days or weeks or more, it is practically impossible to ensure that our unit tests have sufficient coverage. To get real confidence, we need to check more than just a few specific examples. One approach is to take some of the examples that the unit tests are checking and generalise them into a machine-readable specification -- a program that describes how our program should behave. Once we have the specification, we can reformulate it as a set of properties that the program should always satisfy. One such property might be "if the human operator presses the brake, then the accelerator is not active". This property allows us to extend our unit tests to property tests: instead of just checking one example scenario, we can automatically generate hundreds or thousands of different scenarios and check that they all satisfy the property. Property testing allows us to scale unit tests to more testing than a human could feasibly do. For certain classes of programs, we can do even better: we can mathematically prove that the program satisfies the property for all possible scenarios, not just the few thousand scenarios generated by property testing. I am currently implementing an embedded language called Songlark, colloquially lark, which is designed to compile real-time control systems to C and prove them correct.
Songlark is a restricted DSL embedded in Scala. The language allows users to define finite-state automata that run in constant-bounded time and memory. It is strongly inspired by the Lustre dataflow language. Being an embedded language allows us to use a very simple core language without sacrificing too much expressivity, as we get some metalanguage features "for free" such as polymorphism, modules and, to some extent, user-defined types.
We can define simple automata, such as a "bang-bang" controller for a heater. The controller has two states: ON and OFF. It turns the heater element on when the temperature goes below the desired "set-point" temperature, and turns the heater off when the temperature goes above the desired temperature. To avoid oscillating between on and off when the temperature is very close to the desired temperature, we include a hysteresis that makes it a little bit harder to change. The Songlark code for the heater is:
class Heat(setpoint: Stream[Temp], actual: Stream[Temp]) extends Automaton:
val element = output[Bool]
val hysteresis = 5
initial(OFF)
object OFF extends State:
unless {
restart(actual <= setpoint - hysteresis, ON)
}
element := False
object ON extends State:
unless {
restart(actual >= setpoint + hysteresis, OFF)
}
element := True
Once we have the automaton, we can write down some properties that we would like it to have. There isn't too much to say about this simple controller, but one obvious property is that if the temperature is lower than the desired temperature, then the element should be on. To check this property, we add to the definition of the automaton above:
check("heating") {
(actual < setpoint) implies element
}
However, when we check this property, we will see a failure that looks something like:
Node lark.examples.lucid_synchrone.Heater.Heat:
Argument actual: Int16
~~> 1
Argument expected: Int16
~~> 4
element = false
~~> false
Property "heating" at Heater.scala:99 :
actual < expected implies element
~~> false
❌ Property "heating" at Heater.scala:99 : counterexample
The counterexample shows that if the actual temperature is 1 and the expected temperature is 4, then the heating element is off. This behaviour is due to the hysteresis. Correcting the property is simple:
check("heating") {
(actual < setpoint - hysteresis) implies element
}
With the change to take into account the hysteresis, the property passes. Although it's a bit contrived, hopefully this example gives an idea of how even simple controllers can have non-trivial details. When you take many of these simple controllers and compose them together, these little details start to add up in complexity and having an automated way to reason about them pays off.
Songlark is still in the early stages of development and has just reached what I consider to be the "minimum viable product": it supports inductive model checking, integer overflow checks, and compilation to C, but is missing production-quality features such as user-friendly error messages, a foreign function interface, and large-scale verification techniques such as contracts.
The model checking is implemented using an off-the-shelf SMT solver (Z3 by default) as an automated theorem prover. The programs are converted from the core language, which is a streaming dataflow language, to a labelled transition system. The labelled transition system can then be encoded directly in the SMT logic as pure functions for the initial state predicate and step relation.
For generating executable code, I wanted to be as portable as possible for embedded systems. I considered generating LLVM, but decided to generate C as most of the embedded systems I have worked on have used GCC or proprietary C compilers. The potential of having a partially-verified toolchain such as using the CompCert verified C compiler is also somewhat appealing.
There is still much work to do before Songlark is a practical tool. Next, I plan to work on a small, but realistic, example application to get a more concrete understanding of what the current system is missing. For future work, I plan to investigate how to gain more confidence, beyond the current property tests, that the proofs about the labelled transition system really do apply to the generated C code.