Credible Autocoding and Verification of Embedded Software (CrAVES)

Abstract:

Today, the assembly of safety-critical software involves many distinct agents, including control engineers and software engineers. Due in part to the existing regulatory framework, little, if any, semantic information is passed from control engineers (who specify the real-time software) to software engineers (who implement the specifications). As a result, high-level, system-wide information is lost at the time of software assembly, and only during system validation do software specification and semantics re-appear. CrAVES aims at reducing the semantic gap between control engineers and software engineers by introducing a computer-based specification environment that also supports system semantics and their mathematical justification. It then enables the coding of the specifications, together with its semantics, in a verifiable C code. The system semantics supported by CrAVES include system stability, robustness, common performance measures, and fault detection/isolation. It relies on the extensive use of Lyapunov functions, which become inductive invariants at the code level. So far, the autocoding environment has been applied successfully to a variety of aerospace examples, including a 3 degree-of-freedom helicopter and a small turbofan control systems. In both cases, the resulting, semantics-carrying code was shown to successfully control its target hardware in simulation and actual operation. An independant code checking tool was able to check that the code and its semantics were consistent with each other.