Automatic Verification of Linear Controller Software
Publication
, Conference
Pajic, M; Park, J; Lee, I; Pappas, GJ; Sokolsky, O
October 4, 2015
We consider the problem of verification of software implementations of linear time-invariant controllers. Commonly, different implementations use different representations of the controller’s state, for example due to optimizations in a third-party code generator. To accommodate this variation, we exploit input-output controller specification captured by the controller’s transfer function and show how to automatically verify correctness of C code controller implementations using a Frama-C/Why3/Z3 toolchain. Scalability of the approach is evaluated using randomly generated controller specifications of realistic size.
Duke Scholars
DOI
ISBN
978-1-4673-8079-9
Publication Date
October 4, 2015
Start / End Page
217 / 226
Location
Amsterdam, Netherlands
Publisher
IEEE
Conference Name
The ACM SIGBED International Conference on Embedded Software (EMSOFT)
Citation
APA
Chicago
ICMJE
MLA
NLM
Pajic, M., Park, J., Lee, I., Pappas, G. J., & Sokolsky, O. (2015). Automatic Verification of Linear Controller Software (pp. 217–226). Presented at the The ACM SIGBED International Conference on Embedded Software (EMSOFT), Amsterdam, Netherlands: IEEE. https://doi.org/10.1109/EMSOFT.2015.7318277
Pajic, M., J. Park, I. Lee, G. J. Pappas, and O. Sokolsky. “Automatic Verification of Linear Controller Software,” 217–26. IEEE, 2015. https://doi.org/10.1109/EMSOFT.2015.7318277.
Pajic M, Park J, Lee I, Pappas GJ, Sokolsky O. Automatic Verification of Linear Controller Software. In IEEE; 2015. p. 217–26.
Pajic, M., et al. Automatic Verification of Linear Controller Software. IEEE, 2015, pp. 217–26. Manual, doi:10.1109/EMSOFT.2015.7318277.
Pajic M, Park J, Lee I, Pappas GJ, Sokolsky O. Automatic Verification of Linear Controller Software. IEEE; 2015. p. 217–226.
DOI
ISBN
978-1-4673-8079-9
Publication Date
October 4, 2015
Start / End Page
217 / 226
Location
Amsterdam, Netherlands
Publisher
IEEE
Conference Name
The ACM SIGBED International Conference on Embedded Software (EMSOFT)