TY - GEN
T1 - Autocoding control software with proofs I: Annotation translation
AU - Jobredeaux, Romain
AU - Wang, Timothy E.
AU - Feron, Eric M.
N1 - Generated from Scopus record by KAUST IRTS on 2021-02-18
PY - 2011/12/28
Y1 - 2011/12/28
N2 - In an effort to meet the reliability standards that control systems operating in safety-critical roles require, we have started laying the foundation for a tool-set that migrates control theory properties and proofs into the software implementation of those control systems designs. By using this tool the engineer can provide a more rigorous guarantee of the quality of the software and initiate the formal verification process. The tool focuses on control software in order to leverage the domain knowledge from existing mathematical techniques for the analysis and synthesis of control systems. As a first step in the development of the tool-set, we have created a prototype of a Scilab to C translator with proof annotation support. Though limited in its current functionalities, the development of this prototype allowed us to identify the key issues which will be used to further refine the translator. This paper describes the prototype and the further improvements planned for the translator. © 2011 IEEE.
AB - In an effort to meet the reliability standards that control systems operating in safety-critical roles require, we have started laying the foundation for a tool-set that migrates control theory properties and proofs into the software implementation of those control systems designs. By using this tool the engineer can provide a more rigorous guarantee of the quality of the software and initiate the formal verification process. The tool focuses on control software in order to leverage the domain knowledge from existing mathematical techniques for the analysis and synthesis of control systems. As a first step in the development of the tool-set, we have created a prototype of a Scilab to C translator with proof annotation support. Though limited in its current functionalities, the development of this prototype allowed us to identify the key issues which will be used to further refine the translator. This paper describes the prototype and the further improvements planned for the translator. © 2011 IEEE.
UR - http://ieeexplore.ieee.org/document/6096122/
UR - http://www.scopus.com/inward/record.url?scp=84255175689&partnerID=8YFLogxK
U2 - 10.1109/DASC.2011.6096122
DO - 10.1109/DASC.2011.6096122
M3 - Conference contribution
SN - 9781612847979
BT - AIAA/IEEE Digital Avionics Systems Conference - Proceedings
ER -