Proving the correctness of the implementation of a control-command algorithm

Abstract

In this article, we study the interactions between a control-command program and its physical environment via sensors and actuators. We are interested in finding invariants on the continuous trajectories of the physical values that the program is supposed to control. The invariants we are looking for are periodic sequences of intervals that are abstractions of the values read by the program. To compute them, we first build octrees that abstract the impact of the program on its environment. Then, we compute a period of the abstract periodic sequence and we finally define the values of this sequence as the fixpoint of a monotone map. We present a prototype analyzer that computes such invariants for C programs using a simple specification language for describing the continuous environment. It shows good results on classical benchmarks for hybrid systems verification. © 2009 Springer.