Withdraw
Loading…
Certifiable control and verification for safety assurance in cyber-physical systems
Song, Lin
Loading…
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
- Language
- eng
- 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.
- Graduation Semester
- 2024-05
- Type of Resource
- Text
- Handle URL
- https://hdl.handle.net/2142/124573
- Copyright and License Information
- Copyright 2024 Lin Song
Owning Collections
Graduate Dissertations and Theses at Illinois PRIMARY
Graduate Theses and Dissertations at IllinoisManage Files
Loading…
Edit Collection Membership
Loading…
Edit Metadata
Loading…
Edit Properties
Loading…
Embargoes
Loading…