Towards Zero Alarms In Sound Static Analysis Of Finite State Machines

In safety-critical embedded software, the absence of critical code defects has to be demonstrated. One important class of defects are runtime errors caused by undefined or unspecified behavior of the programming language, including buffer overflows or data races. Sound static analyzers can report all such defects in the code (plus some possible false alarms), or prove their absence. A modern sound analyzer is composed of various abstract domains, each covering specific program properties of interest. In this article we present a novel abstract domain developed in the static analyzer Astree. It automatically detects finite state machines and their state variables, and allows to disambiguate the different states and transitions by partitioning. Experimental results on real-life automotive and aerospace code show that embedded control software using finite state machines can be analyzed with close to zero false alarms, and that the improved precision can reduce analysis time.