Automatic Verification of Linear Controller Software

Conference Paper

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.

Full Text

Duke Authors

Cited Authors

  • Pajic, M; Park, J; Lee, I; Pappas, GJ; Sokolsky, O

Published Date

  • October 4, 2015

Start / End Page

  • 217 - 226

Published By

International Standard Book Number 13 (ISBN-13)

  • 978-1-4673-8079-9

Digital Object Identifier (DOI)

  • 10.1109/EMSOFT.2015.7318277

Conference Name

  • The ACM SIGBED International Conference on Embedded Software (EMSOFT)

Conference Location

  • Amsterdam, Netherlands

Conference Start Date

  • October 5, 2015

Conference End Date

  • October 8, 2015