Semantics of Optimization for Real Time Intelligent Embedded Systems (SORTIES)

Abstract:

Optimization algorithms used in a real-time and safety-critical context offer the potential for considerably advancing robotic and autonomous systems by improving their ability to execute complex missions. However, this promise cannot happen without proper attention to the considerably stronger operational constraints that real time, safety-critical applications must meet, unlike their non-real-time, desktop counterparts. Advanced real-time algorithms are growing in complexity and length, related to the growth in autonomy, which allows aircraft, automobile, and medical devices to plan paths of their own. On the other hand, the productivity of safety-critical software developers remains fairly constant at 0.6 to 1 line of code per hour. Knowing that software verification and validation represent fifty percent of their entire engineering development budget, it is then obvious that unless something is done soon, advanced real-time and safety-critical cost development using today's technologies will be unsustainable, if not impossible in the years to come. Then, one of the goal of this project is to demonstrate the relevance and feasibility of embedding modern optimization (and control) algorithms in real-time applications, with strong theoretical guarantees. But also, supporting the expression of proof elements (including on-line optimization modules) to compile those enriched models down to code, carrying along proof elements. Then, this study will seek to develop the capability to re- check this information of proof elements for other purposes, such as verification and documentation. During this project, different work will be studied such as: Proof-Carrying automatic code generation, floating point arithmetic management, nonconvex optimization routines.