2013/08/27 by Timothy C. Wang, Wang, Timothy, Éric Féron +1
Computer Science · Engineering · #FOS: Electrical engineering #Formal Methods in Verification #Modeling and Simulation Systems #Real-time simulation and control systems #Systems and Control (eess.SY) #electronic engineering #information engineering
paper · pdf · doi:10.48550/arxiv.1308.5964
openalex publication_date 2013/08/27 · openalex created_date 2016/06/24 · openalex updated_date 2026/07/28
This article describes the application of a credible autocoding framework for control systems towards a nonlinear car controller example. The framework generates code, along with guarantees of high level functional properties about the code that can be independently verified. These high-level functional properties not only serves as a certificate of good system behvaior but also can be used to guarantee the absence of runtime errors. In one of our previous works, we have constructed a prototype autocoder with proofs that demonstrates this framework in a fully automatic fashion for linear and quasi-nonlinear controllers. With the nonlinear car example, we propose to further extend the prototype's dataflow annotation language environment with with several new annotation symbols to enable the expression of general predicates and dynamical systems. We demonstrate manually how the new extensions to the prototype autocoder work on the car controller using the output language Matlab. Finally, we discuss the requirements and scalability issues of the automatic analysis and verification of the documented output code.