Automatic Software Verification for High-Confidence Cyber-Physical Systems

Presented as part of the 2016 HCSS conference.

ABSTRACT
Software based controllers are at the core of many safety­‐critical embedded and real­-time systems, and thus ensuring their correctness is of paramount importance. To reduce development time and provide some degree of assurance, modern controllers are designed in a model-driven manner; from models of control components, different tools are used to automatically generate control code. On the one hand, verification of control systems and evaluation of the quality of control is typically performed at the modeling level. On the other hand, code generators often provide optimized code to improve system performance, potentially causing discrepancies with the initial model while not affecting input-output behavior of the code. Hence, correctly implemented control software may not satisfy invariants directly derived from the initial model.

To ensure that the generated software implementation of the controller is correct with respect to its model, we ideally would like to have verified code generators that would guarantee that any generated controller correctly implements its model. In practice, however, code generators for control software are complex tools that are not easily amenable to formal verification, and are typically offered as black boxes. One of the reasons is that verification would require ‘transformation­-capturing’ annotations that specify information about employed code optimization techniques, which can cause intellectual property (IP) concerns.

Consequently, our work focuses on techniques for verification of instances of generated code against their model while requiring only input­-output conformance between the code and the initial model. In this talk, we first present our efforts on automatic verification of linear controllers, the
most commonly used type of controllers.
 
We describe techniques to automatically derive software annotations that are insensitive to optimization performed by a code generator. Furthermore, we present methods based on symbolic code execution and equivalence checking to establish proofs of the software correctness from the input-output perspective. Although software verification using the aforementioned techniques is initially performed in the domain of real numbers, we consider imprecise implementations of the controller as a step towards numerical verification of control software.

BIO
Miroslav Pajic is an Assistant Professor in the Department of Electrical & Computer Engineering, Duke University. He also holds a secondary appointment in the Computer Science Department at Duke University. He received his Ph.D. and M.S. degrees in Electrical Engineering from the University of Pennsylvania in 2012 and 2010, and the M.S. and Dipl. Ing. degrees from the University of Belgrade, Serbia, in 2007 and 2003, respectively. Prior to joining Duke in 2015, he was a Postdoctoral Researcher in the PRECISE Center, University of Pennsylvania.

His research interests focus on the design and analysis of cyber-physical systems and in particular real-time and embedded systems, distributed/networked control system, and high-confidence medical device systems. Dr. Pajic received various awards including the 2011 ACM SIGBED Frank Anger Memorial Award, the Joseph and Rosaline Wolf Award for Best Electrical and Systems Engineering Dissertation from Penn Engineering, the Best Paper Award at the 2014 ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS), the Best Student Paper Award at the 2012 IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), and Honeywell User Group Wireless Innovation Award.