Automatic Verification of Finite Precision Implementations of Linear Controllers
Park, Junkil; Pajic, Miroslav; Sokolsky, Oleg; Lee, Insup | April 2017
We consider the problem of verifying finite precision implementation of linear time-invariant controllers against mathematical specifications. A specification may have multiple correct implementations which are different from each other in controller state representation, but equivalent from a perspective of input-output behavior (e.g., due to optimization in a code generator). The implementations may use finite precision computations (e.g. floating-point arithmetic) which cause quantization (i.e., roundoff) errors. To address these challenges, we first extract a controller's mathematical model from the implementation via symbolic execution and floating-point error analysis, and then check approximate input-output equivalence between the extracted model and the specification by similarity checking. We show how to automatically verify the correctness of floating-point controller implementation in C language using the combination of techniques such as symbolic execution and convex optimization problem solving. We demonstrate the scalability of our approach through evaluation with randomly generated controller specifications of realistic size.
CitationPark, Junkil; Pajic, Miroslav; Sokolsky, Oleg; Lee, Insup. 2017. Automatic Verification of Finite Precision Implementations of Linear Controllers. © Think Tanks and Civil Societies Program. http://hdl.handle.net/11540/6963.
Results-Based Monitoring And Evaluation
Project Evaluation & Review Technique
Cumulative effects assessment
Participatory monitoring and evaluationShow allCollapse