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

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. Our goal is to demonstrate the relevance and feasibility of embedding modern optimization (and control) algorithms in real-time applications, with strong theoretical guarantees. Moreover, we want to support the expression of proof elements (including on-line optimization modules) to compile those enriched models down to code, carrying along proof elements. Finally, we would like to develop the capability to re-check this information of proof elements for other purposes, such as verification and documentation.