Motivations and Goals

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):

• Discretization
• Floating-point arithmetic
• 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 de-referencing.