Analysis of Embedded Numerical Programs in the Presence of Numerical Filters

This chapter presents how Frama-C verifies some complex loop invariant for numerical embedded code and how to produce such invariants. Numerical embedded code usually defines an endless loop that takes inputs from sensors and that emits outputs for actuators. Moreover, such a code commonly uses some floating-point global memories to keep track of the input or output values from the previous loop cycles. These memories store a summary of previous values to filter the input or the output over time. Hence, recursive linear or Infinite Impulse Response (IIR) filters are very common in such code. Among such filters, low-pass filters are challenging for Frama-C since finding a loop invariant with complex relationships between the variables is never an evident task for the engineer. Hence, this chapter presents different approaches to find and organize inductive invariants for such numerical reactive systems and shows how Frama-C can prove them with its EvaEva and WpWp plug-ins. It also exposes optimal theoretical results for first-order and higher-order filters to compare the quality of results of the different solutions. Several examples and several concrete solutions illustrate the generation/writing of such inductive invariants and their formal verification.