Formal and Exhaustive Analyses of Numerical Intensive Control Software for Embedded Systems – FEANICSES

As computer power and memory continue to be commoditized, the pressure towards
developing more complex, embedded, safety-critical software keeps
growing. However, the resulting exponential growth of software verification and
validation (V&V) and its certification are significant obstacles; It is often
said that half the development cost of a complex, safety-critical system such as
a commercial aircraft is currently absorbed by software certification. This cost
becomes increasingly unbearable by industry, and may constitute a show-stopper
for emerging systems, such as commercial autonomous unmanned aerial systems and
autonomous cars. Many software V&V challenges can be traced to "intrinsic
complexity", which makes certain advanced, e.g. autonomous, software-borne
technologies out of reach for safety-critical applications.

The FEANICSES project is articulated around the identified need to support the
analysis of system-level properties such as stability, robustness and
performance, at all stages of the system development including code level. The
underlying predicate justifying FEANICSES is that all these properties can be
expressed as numerical invariants over the system states, e.g. using Lyapunov
functions. The approach proposed combines the expression of such properties and
the definition of non linear static analysis techniques.

This interdisciplinary proposal will widely impact the industry practices
supporting the making of safety-critical, software-enabled functions, and
yielding faster convergence towards a consensus about the quality of the
software, and its eventual certification.

FEANICSES results will include an integrated analysis toolchain to analyze
complex cyber-physical systems. The toolchain will support the end-to-end
analysis of a controlled system including its system-level properties. The
toolchain’s final goal is to reduce software certification time and demonstrate
this on several representative use cases.