1 option
Automatic verification of linear controller software / Junkil Park.
LIBRA QA003 2018 .P2351
Available from offsite location
- Format:
- Book
- Manuscript
- Thesis/Dissertation
- Author/Creator:
- Park, Junkil, author.
- Language:
- English
- Subjects (All):
- Penn dissertations--Computer and information science.
- Computer and information science--Penn dissertations.
- Penn dissertations--Education.
- Education--Penn dissertations.
- Local Subjects:
- Penn dissertations--Computer and information science.
- Computer and information science--Penn dissertations.
- Penn dissertations--Education.
- Education--Penn dissertations.
- Physical Description:
- xiv, 126 leaves : illustrations ; 29 cm
- Production:
- [Philadelphia, Pennsylvania] : University of Pennsylvania, 2018.
- Summary:
- 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's 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.
- Notes:
- Ph. D. University of Pennsylvania 2018.
- Department: Computer and Information Science.
- Supervisor: Insup Lee; Oleg Sokolsky.
- Includes bibliographical references.
- OCLC:
- 1240102421
The Penn Libraries is committed to describing library materials using current, accurate, and responsible language. If you discover outdated or inaccurate language, please fill out this feedback form to report it and suggest alternative language.