Skip to main content

· 12 min read
Amos Robinson

This article describes some preliminary work on an invariant generation technique for Lustre. I gave a talk on this at Synchron 2022 in late November 2022. Slides are available here (PDF), but the slides are quite large (25MB) as they contain many bird photographs. I intend to do more evaluation and write this up as a paper in the future.

For safety-critical programs written in Lustre, we can prove that they satisfy certain correctness properties using model checking. Most model checkers for Lustre first transform the program into a transition system and prove properties on the transition system, rather than proving them directly on the streaming semantics of Lustre, because the streaming semantics becomes complex for streams with arbitrary clocks. However, some properties which are obvious on the streaming semantics require extra inductive invariants on the transition system. These invariants may need to refer to internal state of components, which makes them difficult to write in the source language. For such properties, if the model checker's invariant generation techniques do not find the required invariants within the time limit, the proof attempt will time out. I introduce an invariant generation technique called Applicative Invariants for Lustre (AIL) which uses equivalence graphs (e-graphs) to find invariants that hold on the streaming semantics but require inductive invariants on the transition system. This invariant generation technique is designed to work in cooperation with other techniques, as the invariants it proposes are not as diverse as those proposed by instantiation-based invariants [Kahsai11] or counterexample-based invariants such as IC3 [Bradley12]. The advantage is that it draws from a smaller set of possible invariants so that the whole set can be explored exhaustively, making it more resiliant to minor program changes.

· 5 min read
Amos Robinson

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.