Credible Autocoding and Verification of Embedded Software (CrAVES)
Abstract:
The CrAVES project seeks to lay down intellectual foundations for credible autocoding of embedded systems, by which graphical control system specifications that satisfy given open-loop and closed-loop properties are automatically transformed into source code guaranteed to satisfy the same properties. The goal is that the correctness of these codes can be easily and independently verified by dedicated proof checking systems. During the autocoding process, the properties of control system specifications are transformed into proven assertions explicitly written in the resulting source code. Thus CrAVES aims at transforming the extensive safety and reliability analyses conducted by control system engineers, such as those based on Lyapunov theory, into rigorous, embedded analyses of the corresponding software implementations. CrAVES comes as a useful complement to current static software analysis methods, which it leverages to develop independent verification systems. In this poster presentation we will illustrate various results of the CrAVES project:
Crediable compilation: We have developed a tool chain targeting embedded systems developed in Simulink. are directly encoded as Simulink blocks. In a first stage, the toolchain takes as input Simulink models enriched with safety requirements and control semantics such as stability proofs and compiles them either directly to C or to Lustre programs with annotations. In a second stage, the Lustre programs and their annotations are compiled in to C code. For the first phase, we have developed a tool called GAL to perform the compilation; while the compilation for the second phase is done by our tool called LustreC.
Safety verification via model checking: At the Lustre level, we per- form SMT-based model checking to validate the specified safety requirements.
Static and dynamic verification: At the C level, we perform two complementary analysis: (i) static verification to validate for example stability proofs via interactive thorem proving in PVS; (ii) dynamic verification by performing runtime assertion checking on the C code.
Floating point analysis
Case studies: The toolchain has been applied to three case studies: (i) an Engine FADEC (ii) a Fault Tolerant Quanser 3-DOF helicopter and
(iii) the Transport Class Model (TCM).