Automatic Verification of Linear Controller / Junkil Park.
- [Philadelphia, Pennsylvania]: University of Pennsylvania ; Ann Arbor : ProQuest Dissertations & Theses, 2018.
1 online resource (141 pages)
- Local subjects:
- Computer science. (search)
Computer engineering. (search)
Computer and Information Science -- Penn dissertations. (search)
Penn dissertations -- Computer and Information Science. (search)
- System Details:
- Mode of access: World Wide Web.
- 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.
- Source: Dissertation Abstracts International, Volume: 79-10(E), Section: B.
Advisors: Insup Lee; Oleg Sokolsky; Committee members: Rajeev Alur; Mayur Naik; Miroslav Pajic; James Weimer.
Department: Computer and Information Science.
Ph.D. University of Pennsylvania 2018.
- Local notes:
- School code: 0175
- Sokolsky, Oleg, degree supervisor.
Lee, Insup, degree supervisor.
Weimer, James, degree committee member.
Billy the Kid (Singer) degree committee member.
Naik, Mayur, degree committee member.
Alur, Rajeev, degree committee member.
University of Pennsylvania. Computer and Information Science, degree granting institution.
- Contained In:
- Dissertation Abstracts International 79-10B(E).
- Access Restriction:
- Restricted for use by site license.
|Location||Notes||Your Loan Policy|
|Description||Status||Barcode||Your Loan Policy|