Hacker News Reader

Comment by amckinlay | Hacker News Reader

I've always wondered how to use formal verification to prove software on 8 bit microcontrollers. There are so many peripherals like PWM/timers/counters, ADC, UART, and complicated configurations like clock prescalers, self-programming, and interrupts.

View on HN

Not to mention what the clock source is. PLLs (internal or external) can become unlocked. RC oscillators have a lot of temperature dependence.

My most amusing observation of how much this can matter is the obvious obvious pitch/tone change in rail road alerts (at-grade rail crossing signals) on the Metra rail lines around Chicago in the winter. There is a noticeable difference even between 30F and 10F. IIRC correctly (it's been a year since I've been riding the train in the winter), the "beat" of the signal rapidly increases at lower temperatures and the pitch also seems to increase.

Edited for clarity.

Same way it was done long ago: formal specifications with abstract and/or concrete state machines. Each has pre- & post-conditions plus invariants on its behavior. The implementation is simple. Static in terms of memory & such where possible. The resulting FSM's can be analyzed for about all behaviors, including timing. Such a subset is easier to statically analyze for common errors as well. SPARK or Astree can straight-up prove absence of common errors for subsets like that.

I posted a story recently on ASM's that had a simple introduction plus showed some of the temporal logics and such common with them:

https://news.ycombinator.com/item?id=13151828

Depending on your application domain, but if the software has timers and clocks I bet what I'm going to say applies, the good strategy is to use domain specific languages which offer strong guarantee on the produced code. Here I'm thinking specifically of synchronous dataflow languages. Those are formally defined and are designed for critical real-time system. They come with formal verification tools (often, model checkers) adapted to their semantics.

Lustre, Esterel, and Signal, are such languages.

I am aware of some work that involves modelling external devices to achieve verification with SAL or HOL: http://staffwww.dcs.shef.ac.uk/people/R.Taylor/Spurinna/

Reply on news.ycombinator.com