Visible to the public Credible Autocoding and Verification of Embedded Software (CrAVES)


Critical control software is becoming increasingly complex and certification standards increasingly high. In this context it becomes necessary to drive certification costs down while improving safety assurance. We provide a development framework, which draws from control theory concepts and formal analysis to offer a credible, automated control software generation tool. This endeavor, at the intersection of control theory and computer science, aims at bringing together the 2 communities and facilitating their interaction. Indeed it is believed domain specific knowledge can prove itself invaluable in the certification and analysis of generated software.

The challenges are numerous:

  • -- Providing controller designers with easy ways of including stability and performance proofs to their controller diagrams.

  • -- Coming up with a semantic to express stability and performance properties at the level of the code and potentially at intermediate levels of representation of the controller.

  • -- Developing a compiler able to translate these proofs and properties along with the actual controller.

  • -- Study the effect of various model transformations on the validity of the proof (e.g. from an abstraction standpoint):

    SS Discretization
    SS Floating--point arithmetic
    SS Machine--level constructs (pointers)

  • -- Replaying the proofs down at the level of the code in an automatic fashion.

  • -- As the model gets closer to implementation, handle artifacts of concretization such as

    array bound checks and pointer dereferencing.

We have begun answering these questions by working on a framework described in this diagram:

  • -- We have developed an extension to the GeneAuto Simulink to C compiler that is able to transfer stability information from Simulink to C, using new custom blocks at the Simulink level and custom symbols from the ACSL annotation language at the C level.

  • -- From there we have come up with a path to prove the correctness of the annotations in PVS thanks to a linear algebra library.

  • -- The IKOS platform provides a modular way of writing abstract interpreters in order to analyze the generated code for code specific issues. In particular one interpreter was used to look for array bound errors and performed considerably better than available commercial tools.

Award ID: 1135955

Creative Commons 2.5

Other available formats:

Credible Autocoding and Verification of Embedded Software (CrAVES)