Automatic verification of linear controller software
Abstract
© 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.
Type
ConferencePermalink
https://hdl.handle.net/10161/10336Published Version (Please cite this version)
10.1109/EMSOFT.2015.7318277Collections
More Info
Show full item recordScholars@Duke
Miroslav Pajic
Dickinson Family Associate Professor
Miroslav Pajic's research focuses on design and analysis of cyber-physical systems
with varying levels of autonomy and human interaction, at the intersection of (more
traditional) areas of embedded systems, AI, learning and controls, formal methods
and robotics.
Articles written by Duke faculty are made available through the campus open access policy. For more information see: Duke Open Access Policy
Rights for Collection: Scholarly Articles
Works are deposited here by their authors, and represent their research and opinions, not that of Duke University. Some materials and descriptions may include offensive content. More info