How does the ASTREE analyzer deal with digital filters?

Опубликовано 6 сентября 2016, 16:36

The ASTREE analyzer is an abstract interpretation-based static analyzer tailored to prove the absence of run time errors (division by 0, out of bounds, overflow, null pointer dereference, ...) in critical embedded synchronous software as found in earth transportation, nuclear energy, medical instrumentation and aerospace applications. Its design started in November 2001 at the Laboratoire d'Informatique of the Ecole Normale Superieure (LIENS). The ASTREE analyzer was able to prove fully automatically the absence of any run time error in flight control software of fly-by-wire systems. One particularity of the ASTREE analyzer is that it is domain-aware: it knows facts about application domains that are necessary to make sophisticated proofs. One example is the use of specific abstract domains to deal with digital filters. Digital filters are widely used in control/command programs: a digital filter is a numerical algorithm to smooth variations of sampled values of signal. Digital filters involve linear recursions that can hardly be bound by using linear invariants. In contrast, our abstract domains detect digital filters and use both quadratic constraints and formal expansion to bound the ranges of variables in digital filters. In this talk, we will give a short summary of the ASTREE analyzer: we will briefly explain its structure and shortly describe its main abstract domains. Then we will describe the specific framework that deals with digital filtering.