We propose to lay down the intellectual foundations for credible autocoding of control algorithms and their verification, that is, the process by which control system specifications that satisfy given open-loop and closed- loop properties are transformed into source code that is guaranteed to satisfy the same properties. Moreover, the correctness of these codes can be easily and independently verified by dedicated code analyzers. During this process, the properties of control system specifications are therefore transformed into assertions in the resulting source code. Our work aims at transforming the extensive safety and reliability analyses conducted by control system engineers into rigorous, embedded analyses of the corresponding software implementations. It comes as a useful complement to current static software analysis methods, which it leverages to develop independent verification systems. 

Investigators:

Eric Feron (co-PI), Romain Jobredeaux, Timothy Wang, Georgia Institute of Technology

Arnaud Venet (co-PI), Carnegie Mellon University

Pierre-Loïc Garoche, ONERA, France

Marc Pantel, Arnaud Dieumegard, ENSEEIHT, France

Heber Herencia, National Institute of Aerospace