skip to main content

Explore Research Products in the NSF-PAR

Title: Certified Control for Self-Driving Cars.
Certified control is a new architectural pattern for achieving high assurance of safety in autonomous cars. As with a traditional safety controller or interlock, a separate component oversees safety and intervenes to prevent safety violations. This component (along with sensors and actuators) comprises a trusted base that can ensure safety even if the main controller fails. But in certified control, the interlock does not use the sensors directly to determine when to intervene. Instead, the main controller is given the responsibility of presenting the interlock with a certificate that provides evidence that the proposed next action is safe. The interlock checks this certificate, and intervenes only if the check fails. Because generating such a certificate is usually much harder than checking one, the interlock can be smaller and simpler than the main controller, and thus assuring its correctness is more feasible.  more » « less
Award ID(s):
1801399
NSF-PAR ID:
10170076
Author(s) / Creator(s):
; ; ; ; ; ; ;
Date Published:
Journal Name:
DARS 2019: 4th Workshop On The Design And Analysis Of Robust Systems
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. ; ; ; ( , 22nd International Conference on Runtime Verification (RV 2022))
    Dang, Thao ; Stolz, Volker (Ed.)
    We present Barrier-based Simplex (Bb-Simplex), a new, provably correct design for runtime assurance of continuous dynamical systems. Bb-Simplex is centered around the Simplex Control Architecture, which consists of a high-performance advanced controller which is not guaranteed to maintain safety of the plant, a verified-safe baseline controller, and a decision module that switches control of the plant between the two controllers to ensure safety without sacrificing performance. In Bb-Simplex, Barrier certificates are used to prove that the baseline controller ensures safety. Furthermore, Bb-Simplex features a new automated method for deriving, from the barrier certificate, the conditions for switching between the controllers. Our method is based on the Taylor expansion of the barrier certificate and yields computationally inexpensive switching conditions. We consider a significant application of Bb-Simplex to a microgrid featuring an advanced controller in the form of a neural network trained using reinforcement learning. The microgrid is modeled in RTDS, an industry-standard high-fidelity, real-time power systems simulator. Our results demonstrate that Bb-Simplex can automatically derive switching conditions for complex systems, the switching conditions are not overly conservative, and Bb-Simplex ensures safety even in the presence of adversarial attacks on the neural controller. 
    more » « less
  2. ; ; ; ; ( , arXivorg)
    Forward invariance is a long-studied property in control theory that is used to certify that a dynamical system stays within some pre-specified set of states for all time, and also admits robustness guarantees (e.g., the certificate holds under perturbations). We propose a general framework for training and provably certifying robust forward invariance in Neural ODEs. We apply this framework in two settings: certified adversarial robustness for image classification, and certified safety in continuous control. Notably, our method empirically produces superior adversarial robustness guarantees compared to prior work on certifiably robust Neural ODEs (including implicit-depth models). 
    more » « less
  3. ; ; ( , 14th International Conference on Wireless and Mobile Computing, Networking and Communications (WiMob))
    Modern medical devices aim at providing invasive e-health care services to patients with long-term conditions. Typically, these services are implemented as embedded software applications that remotely and automatically control the opera- tions of the devices according to the patient’s condition as mon- itored by the underlying sensors. Such applications are neither safe nor secure mainly because of unreliable sensors, which may provide incorrect input data either due to its malfunctioning or due to some accidental (by privileged user) or intentional (by adversary) interference. Hence, the incorrect sensor data may lead to identification of inaccurate patient condition, which may threaten the patient’s life. To ensure safety and security of e- health applications, current approaches employ data analysis techniques to monitor sensor data and alarm when some unusual value is detected and employ access control strategies to ensure that controller decisions are consistent with sensor input data. However, such approaches fail to detect stealthy attacks, e.g. bad data (false data injection) and bad computations because they do not understand what the application or device is trying to do. To this end, we evaluate our existing approach (i.e., ARMET) to assure safety and security of an emerging and critically real-time application domain of e-health. The approach is based on the specification of the application and device, which has a design and a run-time component. Given an application specification, the design component employs logical verification methods to assure that the application design is resilient to some bad data, i.e., there are no sensor input data values with meaningful threshold which are admissible to the specification but are not true. Given the specification, the runtime component monitors application’s execution and assures that the execution is consistent with the specification and alarms whenever it detects a violation, i.e., there is a bad computation. We evaluate the methodology through its application to an example medical e-health application that controls and monitors blood glucose through an insulin pump. 
    more » « less
  4. ; ; ; ; ; ( , 2021 60th IEEE Conference on Decision and Control (CDC))
    Modern nonlinear control theory seeks to endow systems with properties such as stability and safety, and has been deployed successfully across various domains. Despite this success, model uncertainty remains a significant challenge in ensuring that model-based controllers transfer to real world systems. This paper develops a data-driven approach to robust control synthesis in the presence of model uncertainty using Control Certificate Functions (CCFs), resulting in a convex optimization based controller for achieving properties like stability and safety. An important benefit of our framework is nuanced data-dependent guarantees, which in principle can yield sample-efficient data collection approaches that need not fully determine the input-to-state relationship. This work serves as a starting point for addressing important questions at the intersection of nonlinear control theory and non-parametric learning, both theoretical and in application. We demonstrate the efficiency of the proposed method with respect to input data in simulation with an inverted pendulum in multiple experimental settings. 
    more » « less
  5. ; ( , IEEE)
    This paper considers the problem of learning models to be used for controller design. Using a simple example, it argues that in this scenario the objective should reflect the closed-loop, rather than open-loop distance between the learned model and the actual plant, a task that can be accomplished by using a gap metric motivated approach. This is particularly important when identifying open-loop unstable plants, since typically in this case the open-loop distance is unbounded. In this context, the paper proposes a convex optimization approach to learn its coprime factors. This approach has a dual advantage: (1) it can easily handle open-loop unstable plants, since the coprime factors are stable, and (2) it is "self certified", since a simple norm computation on the learned factors indicates whether or not a controller designed based on these factors will stabilize the actual (unknown) plant. If this test fails, it indicates that further learning is needed. 
    more » « less
  • Citation Formats
  • MLA
  • APA
  • Chicago
  • BibTeX
  • Save / Share this Record
  • Send to Email