Certifiable control and verification for safety assurance in cyber-physical systems

Song, Lin

Permalink

https://hdl.handle.net/2142/124573 Copy

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