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.
