Automatic Verification of Linear Controller

Many safety-critical cyber-physical systems have a software-based controller at their core. Since the system behavior relies on the operation of the controller, it is imperative to ensure the correctness of the controller to have a high assurance for such systems. Nowadays, controllers are developed in a model-based fashion. Controller models are designed, and their performances are analyzed first at the model level. Once the control design is complete, software implementation is automatically generated from the mathematical model of the controller by a code generator. To assure the correctness of the controller implementation, it is necessary to check that the code generation is correctly done. Commercial code generators are complex black-box software that are generally not formally verified. Subtle bugs have been found in commercially available code generators that consequently generate incorrect code. In the absence of verified code generators, it is desirable to verify instances of implementations against their original models. Such verification is desired to be performed from the input-output perspective because correct implementations may have different state representations to each other for several possible reasons (e.g., code generator\u27s choice of state representation, optimization used in code generator and code transformation). In this dissertation, we propose several methods to verify a given controller implementation against its given model from the input-output perspective. First of all, we propose a method to derive assertions from the controller model, and check if the assertions are invariant to the controller implementation via a proposed toolchain based on a popular deductive program verification framework. Moreover, we propose an alternative more scalable method that extracts a model from the controller implementation using the symbolic execution technique, and compare the extracted model to the original controller model using state-of-the-art constraint solvers. Lastly, we extend our latter method to correctly account for the rounding errors in the floating-point computation of the controller implementation. We demonstrate the scalability of our proposed approaches through evaluation with randomly generated controller specifications of realistic size