Automatic verification of linear controller software
Repository Usage Stats
© 2015 IEEE.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.
Published Version (Please cite this version)10.1109/EMSOFT.2015.7318277
More InfoShow full item record
Dickinson Family Associate Professor
Miroslav Pajic's research focuses on design and analysis of cyber-physical systems and in particular, embedded and distributed/networked control, real-time and embedded systems, and high-confidence medical device systems.