Verification of fast optimization algorithms applied in critical embedded control – VORACE

Optimization algorithms, when they are used in a real-time and safety-critical context, offer the potential for considerably advancing robotic and autonomous systems by enabling significant improvements in their ability to initiate, plan, and execute complex missions. In that regard, they are likely to realize the same promise as that delivered long ago by the desktop application of optimization algorithms. However, this promise cannot happen without proper attention to the considerably stronger operational constraints that real-time, safety-critical application must meet, unlike
their non real-time, desktop counterparts. In particular, safety-critical real-time optimization algorithms must be equipped with deterministic bounds on their worst-case execution time (WCET); Absence of run-time errors, such as variable range overflows and divide-by zero errors, must be systematically analyzed and eliminated. Finally, the semantics of optimization algorithms, that is, what they actually do, must be systematically documented and accessible at all implementation levels, ranging from specification documents to binary executables. Such semantics may be complex to obtain when the original purpose of the optimization algorithms is combined with real-world computational imperfections, such as floating-point number approximation and computation.

We therefore propose a comprehensive study aimed at defining the suitability of
optimization algorithms to meet the stringent constraints that must be met by
real-time safety critical software.

The study will begin by reviewing the existing literature, which includes the
enormous amount of research performed on the performance of optimization
algorithms. This literature search will be performed in the light of the
certification requirements briefly described above, and their applicability to
actual autonomous missions. In particular, the time-complexity of these
algorithms, and their stability analyses may prove critical to their usability
in a real-time framework. The current state-of-the art in optimization algorithm
implementation will also be examined.

The study will then continue with a detailed study of how optimization
algorithms, and their implementations, may be modified to meet real-time
implementation requirements. For that purpose, optimization algorithm complexity
will be re-examined, having imperfect computations in mind. Theoretical
frameworks used in computer science will be leveraged to document the codes that
implement optimization routines in a way that explicitly supports its
performance and semantics. Such frameworks may include Hoare's logic, which is
well-adapted to the sequential implementation of optimization algorithms that we
intend to examine first. We will initiate our work with finite-dimensional,
convex optimization routines, because of the extensive literature available
about them, and also because of their extensive usability in a broad range of
applications ranging from receding-horizon control to optimal route-finding.

The study will then continue with the building of a prototype tool aimed at
producing verifiable implementations of optimization algorithms. Beginning with
convex optimization algorithms, we will leverage and revisit recent work aiming
at automatically producing executable optimization algorithms from broad
specifications. We will include the automatic documentation of the software
implementation of these algorithms. We will then place such documented algorithms
through software analysis procedure and compare the resulting analyses with
those that may be obtained from equivalent, but undocumented, software.