Certifiable control and verification for safety assurance in cyber-physical systems
Song, Lin
This item is only available for download by members of the University of Illinois community. Students, faculty, and staff at the U of I may log in with your NetID and password to view the item. If you are trying to access an Illinois-restricted dissertation or thesis, you can request a copy through your library's Inter-Library Loan office or purchase a copy directly from ProQuest.
Permalink
https://hdl.handle.net/2142/124573
Description
Title
Certifiable control and verification for safety assurance in cyber-physical systems
Author(s)
Song, Lin
Issue Date
2024-04-24
Director of Research (if dissertation) or Advisor (if thesis)
Hovakimyan, Naira
Doctoral Committee Chair(s)
Hovakimyan, Naira
Committee Member(s)
Mitra, Sayan
Salapaka, Srinivasa M.
Zhang, Huan
Department of Study
Mechanical Sci & Engineering
Discipline
Mechanical Engineering
Degree Granting Institution
University of Illinois at Urbana-Champaign
Degree Name
Ph.D.
Degree Level
Dissertation
Keyword(s)
Control and Optimization
Formal Verification
Safety Assurance
Abstract
Cyber-physical systems (CPSs) integrate physical systems with computational elements and find applications in various domains, including robotics, industrial automation, and autonomous vehicles. While significant advances have been made in CPS research, ensuring their reliable and dependable performance in safety-critical scenarios remains a challenge, due to their complex dynamics and the necessity for interdisciplinary approaches. The research proposed in this dissertation aims to establish safety assurance in autonomous systems at multiple levels, employing control theory, formal verification, machine learning, and optimization. At the low level, we present a certifiable control development framework for networked systems that enhances computational efficiency while ensuring safety by design. This framework enables the computation of composite control for new tasks using existing controllers, leveraging the system's linear-solvable and compositionality properties. Following that, the framework is extended to unconstrained optimization formulations by incorporating barrier state (BaS) encoding control barrier function (CBF) constraints into the joint dynamics of networked systems, thus preserving control solution optimality. Additionally, the dissertation explores the use of satisfiability modulo theories (SMT)-based planners for synthesizing piecewise linear (PWL) reference trajectories to guide the optimal control task, offering an alternative solution to maintain control optimality. The dissertation also delves into the application of formal verification techniques to verify performance guarantees and safety assurance in model-based control algorithms. The evaluation of controller performance and bounded safety is conducted by analyzing the dimensions of reachable states computed from existing verification tools under various scenarios. For instance, we first formally verify the robustness margin guarantees and systematic design guidelines in the L_1 Adaptive Control (L_1 AC) framework. The verification experiments span from laboratory-sized quadrotors to real-world high-fidelity Lift-Plus-Cruise (L+C) vehicles. At a higher level, the dissertation focuses on improving the safety of autonomous vehicles during the planning phase. It proposes computationally efficient approaches for generating safe trajectories and making decisions for vehicles in dense traffic, where safe interaction is crucial. The proposed approach achieves safety, feasibility, and real-time computational efficiency in trajectory generation by integrating data-driven reasoning with model-based particle swarm optimization (PSO) techniques, showing great potential for hardware deployment.
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.