Program

All times indicated below are in Central Time (CT).
Beijing is 13 hours ahead of CT.
Milano is 7 hours ahead of CT

Session Chair: Miroslav Pajic

• Confidence Composition for Monitors of Verification Assumptions, Ivan Ruchkin, Matthew Cleaveland, Radoslav Ivanov, Pengyuan Lu, Taylor Carpenter, Oleg Sokolsky, Insup Lee (University of Pennsylvania)
  • pre-recorded video (password protected)

  Abstract

  Confidence Composition for Monitors of Verification Assumptions

  • Ivan Ruchkin, University of Pennsylvania
  • Matthew Cleaveland, University of Pennsylvania
  • Radoslav Ivanov, University of Pennsylvania
  • Pengyuan Lu, University of Pennsylvania
  • Taylor Carpenter, University of Pennsylvania
  • Oleg Sokolsky, University of Pennsylvania
  • Insup Lee, University of Pennsylvania

  Closed-loop verification of cyber-physical systems with neural network controllers offers strong safety guarantees under certain assumptions. It is, however, difficult to determine whether these guarantees apply at run time because verification assumptions may be violated. To predict safety violations in a verified system, we propose a three-step framework for monitoring the confidence in verification assumptions. First, we represent the sufficient condition for verified safety with a propositional logical formula over assumptions. Second, we build calibrated confidence monitors that evaluate the probability that each assumption holds. Third, we obtain the confidence in the verification guarantees by composing the assumption monitors using a composition function suitable for the logical formula. Our framework provides theoretical bounds on the calibration and conservatism of compositional monitors. In two case studies, we demonstrate that the composed monitors improve over their constituents and successfully predict safety violations.

• Automatic Generation of Test-cases of Increasing Complexity for Autonomous Vehicles at Intersections, Abolfazl Karimi, Parasara Sridhar Duggirala (University of North Carolina)
  • pre-recorded video (password protected)

  Abstract

  Automatic Generation of Test-cases of Increasing Complexity for Autonomous Vehicles at Intersections

  • Abolfazl Karimi, University of North Carolina
  • Parasara Sridhar Duggirala, University of North Carolina

  This paper presents a new framework for generating test-case scenarios for autonomous vehicles. We address two challenges in automatic test-case generation: first, a formal notion of test-case complexity, and second, an algorithm to generate more-complex test-cases. We characterize the complexity of a test-case by its set of solutions, and compare two complexities by the subset relation. The novelty of our definition is that it only relies on the pass-fail criteria of the test-case, rather than indirect or subjective assessments of what may challenge an ego vehicle to pass a test-case. Given a test-case, we model the problem of generating a more complex test-case as a constraint-satisfaction search problem. The search variables are the changes to the given test-case, and the search constraints define a solution to the search problem. The constraints include steering geometry of cars, the geometry of lanes, the shape of cars, traffic rules, bounds on longitudinal acceleration of cars, etc. To conquer the computational challenge, we divide the constraints to three categories and satisfy them with simulation, answer set programming, and SMT solving. We have implemented our algorithm using the Scenic libraries and the CARLA simulator and generate test-cases for several 3-way and 4-way intersections with different topologies. Our experiments demonstrate that both CARLA’s autopilot and autopilot-plus-RSS Responsibility-Sensitive Safety) can fail as the complexity of test-cases increase.

• Coverage-Guided Fuzz Testing for Cyber-Physical Systems, Sanaz Sheikhi, Edward Kim, Parasara Sridhar Duggirala, Stanley Bak (SUNY Stony Brook,University of North Carolina – Chapel Hill)
  • pre-recorded video (password protected)

  Abstract

  Coverage-Guided Fuzz Testing for Cyber-Physical Systems

  • Sanaz Sheikhi, SUNY Stony Brook
  • Edward Kim, University of North Carolina – Chapel Hill
  • Parasara Sridhar Duggirala, University of North Carolina – Chapel Hill
  • Stanley Bak, SUNY Stony Brook

  Fuzz testing is an indispensable test-generation tool in software security. Fuzz testing uses automated directed randomness to explore a variety of execution paths in software, trying to expose defects such as buffer overflows. Since cyber-physical systems (CPS) are often safety-critical, testing models of CPS can also expose faults. However, while existing coverage-guided fuzz testing methods are effective for software, results can be disappointing when applied to CPS, where systems have continuous states and inputs are applied at different points in time. In this work, we propose three changes to customize coverage-guided fuzz testing methods to better leverage characteristics of CPS. First, we introduce a notion of coverage that be used to evaluate a fuzz testing algorithm’s effectiveness for a particular CPS, analogous to often-used code coverage metrics of a software system. Second, this modified coverage metric is used in a customized power schedule, which selects which previous input sequences hold the most promise to find failures in new system states. Third, we modify the input mutation strategy used to reason with the causal nature of a CPS. We call the approach CPSFuzz and evaluate it on a simulation environment used for the F1TENTH autonomous car racing competition, attempting to find collisions during head-to-head racing. Compared with both using existing software fuzz testing tools and random test generation, CPSFuzz generates more crashes at different positions around the track.

• Querying Images with Scenario Programs for Sim-to-Real Validation, Edward Kim, Jay Shenoy, Sebastian Junges, Daniel Fremont, Alberto Sangiovanni-Vincentelli, Sanjit Seshia (UC Berkeley, UC Santa Cruz, Radboud University)
  • pre-recorded video (password protected)

  Abstract

  Querying Images with Scenario Programs for Sim-to-Real Validation

  • Edward Kim, University of California, Berkeley
  • Jay Shenoy, University of California, Berkeley
  • Sebastian Junges, Radboud University
  • Daniel Fremont, University of California, Santa Cruz
  • Alberto Sangiovanni-Vincentelli, University of California, Berkeley
  • Sanjit Seshia, University of California, Berkeley

  Simulation-based testing of autonomous vehicles (AVs) has become an essential complement to road testing to ensure safety. Consequently, substantial research has focused on searching for failure scenarios in simulation. However, a fundamental question remains: are AV failure scenarios identified in simulation meaningful in reality — i.e., are they reproducible on the real system? Due to the sim-to-real gap arising from discrepancies between simulated and real sensor data, a failure scenario identified in simulation can be either a spurious artifact of the synthetic sensor data or an actual failure that persists with real sensor data. One approach to validate simulated failure scenarios is to identify instances of the scenario in a corpus of real data, and check if the failure persists on the real data. Towards this end, we propose a formal definition of what it means for a labelled data point to match an abstract scenario, encoded as a scenario program using the SCENIC probabilistic programming language. Using this definition, we develop a querying algorithm which, given a scenario program and a labelled dataset, finds the subset of the data matching the scenario. Experiments demonstrate that our algorithm is accurate and efficient on a variety of realistic traffic scenarios, and scales to a reasonable number of agents.

Session Chair: Stanley Bak

• Blind Spots of Objective Measures: Exploiting Imperceivable Errors for Immersive Tactile Internet, Herman Kroep, Vineet Gokhale, R. Venkatesha Prasad (TU Delft)
  • pre-recorded video (password protected)

  Abstract

  Blind Spots of Objective Measures: Exploiting Imperceivable Errors for Immersive Tactile Internet

  • Herman Kroep, TU Delft
  • Vineet Gokhale, TU Delft
  • R. Venkatesha Prasad, TUDelft

  Tactile Internet (TI) enables the transfer of human skills across the Internet by enabling teleoperation with force feedback. Advancements are being made rapidly at several fronts to realize a functional TI soon. Generally, TI expects faithful reproduction of the operator’s action at the other end, where a robotic arm emulates it while providing force feedback to the operator. Performance of TI is usually characterized using objective metrics such as network delay, RMSE, and packet losses. Pari passu, subjective evaluations are used as additional validation, and performance evaluation itself is not primarily based on user experience. Hence objective evaluation, which generally minimizes error (signal mismatch) is oblivious to subjective experience. In this paper, we argue that user-centric designs of TI solutions are necessary. We first consider a few common TI errors and examine their perceivability. The idea is to reduce the impact of perceivable errors and exploit the imperceivable errors for our advantage, while the objective metrics may indicate that the errors are high. To harness the imperceivable errors, we design Adaptive Offset Framework (AOF) to improve the TI signal reconstruction under realistic network settings. We use AOF to highlight the contradictory inferences drawn by objective and subjective evaluations while realizing that subjective evaluations are closer to ground truth. This strongly suggests the existence of blind spots of objective measures’. Further, we show that AOF significantly improves the user grade, up to 3 points (on a scale of 10) in comparison with the standard reconstruction method.

• Infrastructure-free, Deep Learned Urban Noise Monitoring at ∼100mW, Jihoon Yun, Sangeeta Srivastava, Dhrubojyoti Roy, Nathan Stohs, Charlie Mydlarz, Mahin Salman, Bea Steers, Juan Pablo Bello, Anish Arora (The Ohio State University,New York University)
  • pre-recorded video (password protected)

  Abstract

  Infrastructure-free, Deep Learned Urban Noise Monitoring at ∼100mW

  • Jihoon Yun, The Ohio State University
  • Sangeeta Srivastava, The Ohio State University
  • Dhrubojyoti Roy, The Ohio State University
  • Nathan Stohs, The Samraksh Company
  • Charlie Mydlarz, New York University
  • Mahin Salman, New York University
  • Bea Steers, New York University
  • Juan Pablo Bello, New York University
  • Anish Arora, The Ohio State University

  The Sounds of New York City (SONYC) wireless sensor network(WSN) has been fielded in Manhattan and Brooklyn over the past five years, as part of a larger human-in-the-loop cyberphysical control system for monitoring, analyzing, and mitigating urban noise pollution. We describe the evolution of the 2-tier SONYC WSN from an acoustic data collection fabric into a 3-tier in situ noise complaint monitoring WSN, and its current evaluation. The added tier consists of long range (LoRA), multi-hop networks of a new low-power acoustic mote, MKII (“Mach 2”), that we have designed and fabricated. MKII motes are notable in three ways: First, they advance machine learning capability at mote-scale in this application domain by introducing a real-time CNN embedding model that is competitive with alternatives while also requiring 10×lesser training data and∼2 orders of magnitude fewer run-time resources. Second, they are conveniently deployed relatively far from higher tier base station nodes without assuming power or network infrastructure support at operationally relevant sites(such as construction zones), yielding a relatively low cost solution.And third, their networking is frequency agile, unlike conventionalLoRa networks: it tolerates in a distributed, self-stabilizing way the variable external interference and link fading in the cluttered 902-928MHz ISM band urban environment by dynamically choosing good frequencies using an efficient new method that combines passive and active measurements.

• HydraFusion: Context-Aware Selective Sensor Fusion for Robust and Efficient Autonomous Vehicle Perception, Arnav Vaibhav Malawade, Trier Mortlock, Mohammad Al Faruque (UC Irvine)
  • pre-recorded video (password protected)

  Abstract

  HydraFusion: Context-Aware Selective Sensor Fusion for Robust and Efficient Autonomous Vehicle Perception

  • Arnav Vaibhav Malawade, UC Irvine
  • Trier Mortlock, UC Irvine
  • Mohammad Al Faruque, UC Irvine

  Although autonomous vehicles (AVs) are expected to revolutionize transportation, robust perception across a wide range of driving contexts remains a significant challenge. Techniques to fuse sensor data from camera, radar, and lidar sensors have been proposed to improve AV perception. However, existing methods are insufficiently robust in difficult driving contexts (e.g., bad weather, low light, sensor obstruction) due to rigidity in their fusion implementations. These methods fall into two broad categories: (i) early fusion, which fails when sensor data is noisy or obscured, and (ii) late fusion, which cannot leverage features from multiple sensors and thus produces worse estimates. To address these limitations, we propose HydraFusion a selective sensor fusion framework that learns to identify the current driving context and fuses the best combination of sensors to maximize robustness without compromising efficiency. HydraFusion is the first approach to propose dynamically adjusting between early fusion, late fusion, and combinations in-between, thus varying both how and when fusion is applied. We show that, on average, HydraFusion outperforms early and late fusion approaches by 13.66% and 14.54%, respectively, without increasing computational complexity or energy consumption on the industry-standard Nvidia Drive PX2 AV hardware platform. We also propose and evaluate both static and deep-learning-based context identification strategies. Our open-source code and model implementation are available at https://anonymous.4open.science/r/hydrafusion/.

• Offline Policy Evaluation for Learning-based Deep BrainStimulation Controllers, Qitong Gao, Stephen L. Schmidt, Karthik Kamaravelu, Dennis A. Turner, Warren M. Grill, Miroslav Pajic (Duke University)
  • pre-recorded video (password protected)

  Abstract

  Offline Policy Evaluation for Learning-based Deep BrainStimulation Controllers

  • Qitong Gao, Duke University
  • Stephen L. Schmidt, Duke University
  • Karthik Kamaravelu, Duke University
  • Dennis A. Turner, Duke University
  • Warren M. Grill, Duke University
  • Miroslav Pajic, Duke University

  Deep brain stimulation (DBS) is an effective procedure to treat motor symptoms caused by nervous system disorders such as Parkinson’s disease (PD). Although existing implantable DBS devices can suppress PD symptoms by delivering fixed periodic stimuli to the Basal Ganglia (BG) region of the brain, they are considered inefficient in terms of energy and could cause side-effects. Recently, reinforcement learning (RL)-based DBS controllers have been developed to achieve both stimulation efficacy and energy efficiency, by adapting stimulation parameters (e.g., pattern and frequency of stimulation pulses) to the changes in neuronal activity. However, RL methods usually provide limited safety and performance guarantees, and directly deploying them on patients may be hindered due to clinical regulations. Thus, in this work, we introduce a model-based offline policy evaluation (OPE) methodology to estimate the performance of RL policies using historical data. As a first step, the BG region of the brain is modeled as a Markov decision process (MDP). Then, a deep latent MDP (DL-MDP) model is learned using variational inference and previously collected control trajectories. The performance of RL controllers is then evaluated on the DL-MDP models instead of patients directly, ensuring safety of the evaluation process. Further, we show that our method can be integrated into offline RL frameworks, improving control performance when limited training data are provided. We illustrate the use of our methodology on a computational Basal Ganglia model (BGM); we show that it accurately estimates the expected returns of controllers trained following state-of-the-art RL frameworks, outperforming existing OPE methods designed for general applications.

Session Chair: Abhishek Dubey

• Monotonic Safety for Scalable and Data-Efficient Probabilistic Safety Analysis, Matthew Cleaveland, Ivan Ruchkin, Oleg Sokolsky, Insup Lee (University of Pennsylvania)
  • pre-recorded video (password protected)

  Abstract

  Monotonic Safety for Scalable and Data-Efficient Probabilistic Safety Analysis

  • Matthew Cleaveland, University of Pennsylvania
  • Ivan Ruchkin, University of Pennsylvania
  • Oleg Sokolsky, University of Pennsylvania
  • Insup Lee, University of Pennsylvania

  Autonomous systems with machine learning-based perception can exhibit unpredictable behaviors that are difficult to quantify, let alone verify. Such behaviors are convenient to capture in probabilistic models, but model checking of such models is difficult to scale — largely due to the non-determinism added to models as a prerequisite for provable conservatism. Statistical model checking (SMC) has been proposed to address the scalability issue. However it requires large amounts of data to account for the aforementioned non-determinism, which in turn limits its scalability. This work introduces a general technique for reduction of non-determinism based on assumptions of “monotonic safety”, which define a partial order between system states in terms of their probabilities of being safe. We exploit these assumptions to remove non-determinism from controller\/plant models to drastically speed up probabilistic model checking and statistical model checking while providing provably conservative estimates as long as the safety is indeed monotonic. Our experiments demonstrate model-checking speed-ups of an order of magnitude while maintaining acceptable accuracy and require much less data for accurate estimates when running SMC — even when monotonic safety does not perfectly hold and provable conservatism is not achieved.

• Verifying Safety for Resilient Cyber-Physical Systems via Reactive Software Restart, Luyao Niu, Dinuka Sahabandu, Andrew Clark, Radha Poovendran (Worcester Polytechnic Institute)
  • pre-recorded video (password protected)

  Abstract

  Verifying Safety for Resilient Cyber-Physical Systems via Reactive Software Restart

  • Luyao Niu, Worcester Polytechnic Institute
  • Dinuka Sahabandu, University of Washington
  • Andrew Clark, Worcester Polytechnic Institute
  • Radha Poovendran, Department of Electrical Engineering, University of Washington

  Resilient cyber-physical systems (CPS) must ensure safety and perform required tasks in the presence of malicious cyber attacks. Recently, restart-based defenses have been proposed in which a CPS mitigates attacks by reverting to an initial safe state. In this paper, we consider a class of reactive restart approaches for CPS under malicious attacks with verifiable safety guarantees. We consider a setting where the controllers are engineered to crash and reboot following faults or attacks. We present a hybrid system model that captures the trade-off between security, availability, and safety of the CPS due to the reactive restart. We develop sufficient conditions under which an affine controller provides verifiable safety guarantees for the physical plant using a barrier certificate approach. We synthesize safety-critical controllers using control barrier functions to guarantee system safety under given timing parameters. We present two case studies on the proposed approach using a warehouse temperature control system and a two-dimensional non-linear system. Our proposed approach guarantees the safety for both cases.

• Statistical Verification of Cyber-Physical Systems using Surrogate Models and Conformal Inference, Xin Qin, Yuan Xia, Chuchu Fan, Jyotirmoy Deshmukh, Aditya Zutshi (University of Southern California, MIT)
  • pre-recorded video (password protected)

  Abstract

  Statistical Verification of Cyber-Physical Systems using Surrogate Models and Conformal Inference

  • Xin Qin, University of Southern California
  • Yuan Xia, University of Southern California
  • Chuchu Fan, Massachusetts Institute of Technology
  • Jyotirmoy Deshmukh, University of Southern California
  • Aditya Zutshi, Galois

  In this paper, we proposa a new approach for statistical verification of parametric black-box CPS models with a user-provided distribution on the model parameters. Our technique uses model simulations to learn surrogate models, and uses conformal in-ference to provide probabilistic guarantees on the satisfaction of a given STL property. Additionally, we can provide prediction intervals containing the quantitative satisfaction values of the given STL property for any user-specified confidence level. We also propose a refinement procedure based on Gaussian Process (GP)-based surrogate models for obtaining fine-grained probabilistic guarantees over sub-regions in the parameter space. This in turn enables the CPS designer to choose assured validity domains in the parameter space for safety-critical applications. Finally,we demonstrate the efficacy of our technique on several CPS models.

• Safety from Fast, In-the-Loop Reachability with Application to UAVs, Christian Llanes, Matthew Abate, Samuel Coogan (Georgia Institute of Technology)
  • pre-recorded video (password protected)

  Abstract

  Safety from Fast, In-the-Loop Reachability with Application to UAVs

  • Christian Llanes, Georgia Institute of Technology
  • Matthew Abate, Georgia Institute of Technology
  • Samuel Coogan, Georgia Institute of Technology

  We present a runtime assurance (RTA) mechanism for ensuring safety of a controlled dynamical system and an application to collision avoidance of two unmanned aerial vehicles (UAVs). We consider a dynamical system controlled by an unverified and potentially unsafe primary controller that might, e.g., lead to collision. The proposed RTA mechanism computes at each time the reachable set of the system under a backup control law. We then develop a novel optimization problem based on control barrier functions that filters the primary controller when necessary in order to keep the system’s reachable set within reach of a known, but conservative, safe region. The theory of mixed monotone systems is leveraged for efficient reachable set computation and to achieve a tractable optimization formulation. We demonstrate the proposed RTA mechanism on a dual multirotor UAV case study which requires a fast controller update rate as a result of the small time-scale rotational dynamics. In implementation, the algorithm computes the reachable set of an eight dimensional dynamical system in less than five milliseconds and solves the optimization problem in under one millisecond, yielding a controller update rate of 100Hz.

Session Chair: Pavithra Prabhakar

• Physics-Aware Safety-Assured Design of Hierarchical Neural Network based Planner, Xiangguo Liu, Chao Huang, Yixuan Wang, Bowen Zheng, Qi Zhu (Northwestern University, University of Liverpool)
  • pre-recorded video (password protected)

  Abstract

  Physics-Aware Safety-Assured Design of Hierarchical Neural Network based Planner

  • Xiangguo Liu, Northwestern University
  • Chao Huang, University of Liverpool
  • Yixuan Wang, Northwestern University
  • Bowen Zheng, Pony.ai
  • Qi Zhu, Northwestern University

  Neural networks have shown great promises in planning, control, and general decision making for learning-enabled cyber-physical systems (LE-CPSs), especially in improving performance under complex scenarios. However, it is very challenging to formally analyze the behavior of neural network based planners for ensuring system safety, which significantly impedes their applications in safety-critical domains such as autonomous driving. In this work, we propose a hierarchical neural network based planner that analyzes the underlying physical scenarios of the system and learns a system-level behavior planning scheme with multiple scenario-specific motion-planning strategies. We then develop an efficient verification method that incorporates overapproximation of the system state reachable set and novel partition and union techniques for formally ensuring system safety under our physics-aware planner. With theoretical analysis, we show that considering the different physical scenarios and building a hierarchical planner based on such analysis may improve system safety and verifiability. We also empirically demonstrate the effectiveness of our approach and its advantage over other baselines in practical case studies of unprotected left turn and highway merging, two common challenging safety-critical tasks in autonomous driving.

• An Online Approach to Solve the Dynamic Vehicle Routing Problem with Stochastic Trip Requests for Paratransit Services, Michael Wilbur, Salah Uddin Kadir, Youngseo Kim, Geoff Pettet, Ayan Mukhopadhyay, Philip Pugliese, Samitha Samaranayake, Aron Laszka, Abhishek Dubey (Vanderbilt University, University of Houston, Cornell University)
  • pre-recorded video (password protected)

  Abstract

  An Online Approach to Solve the Dynamic Vehicle Routing Problem with Stochastic Trip Requests for Paratransit Services

  • Michael Wilbur, Vanderbilt University
  • Salah Uddin Kadir, University of Houston
  • Youngseo Kim, Cornell University
  • Geoff Pettet, Vanderbilt University
  • Ayan Mukhopadhyay, Vanderbilt University
  • Philip Pugliese, Chattanooga Area Regional Transportation Authority (CARTA)
  • Samitha Samaranayake, Cornell University
  • Aron Laszka, University of Houston
  • Abhishek Dubey, Vanderbilt University

  Many transit agencies operating paratransit and microtransit services have to respond to trip requests that arrive in real-time, which entails solving hard combinatorial and sequential decision-making problems under uncertainty. To avoid decisions that lead to significant inefficiency in the long term, vehicles should be allocated to requests by optimizing a non-myopic utility function or by batching requests together and optimizing a myopic utility function. While the former approach is typically offline, the latter can be performed online. We point out two major issues with such approaches when applied to paratransit services in practice. First, it is difficult to batch paratransit requests together as they are temporally sparse. Second, the environment in which transit agencies operate changes dynamically (e.g., traffic conditions can change over time), causing the estimates that are learned offline to become stale. To address these challenges, we propose a fully online approach to solve the dynamic vehicle routing problem (DVRP) with time windows and stochastic trip requests that is robust to changing environmental dynamics by construction. We focus on scenarios where requests are relatively sparse—our problem is motivated by applications to paratransit services. We formulate DVRP as a Markov decision process and use Monte Carlo tree search to compute near-optimal actions for any given state. Accounting for stochastic requests while optimizing a non-myopic utility function is computationally challenging; indeed, the action space for such a problem is intractably large in practice. To tackle the large action space, we leverage the structure of the problem to design heuristics that can sample promising actions for the tree search. Our experiments using real-world data from our partner agency show that the proposed approach outperforms existing state-of-the-art approaches both in terms of performance and robustness.

• Toward Physics-Guided Safe Deep Reinforcement Learning for Green Data Center Cooling Control, Ruihang Wang, Xinyi Zhang, Xin Zhou, Yonggang Wen, Rui Tan (Nanyang Technological University)
  • pre-recorded video (password protected)

  Abstract

  Toward Physics-Guided Safe Deep Reinforcement Learning for Green Data Center Cooling Control

  • Ruihang Wang, Nanyang Technological University
  • Xinyi Zhang, Nanyang Technological University
  • Xin Zhou, Nanyang Technological University
  • Yonggang Wen, Nanyang Technological University
  • Rui Tan, Nanyang Technological University

  Deep reinforcement learning (DRL) has shown good performance in tackling Markov decision process (MDP) problems. As DRL optimizes a long-term reward, it is a promising approach to improving the energy efficiency of data center cooling. However, enforcement of thermal safety constraint during DRL’s state exploration is a main challenge. The widely adopted reward shaping approach adds negative reward when the exploratory action results in unsafety. Thus, it needs to experience sufficient unsafe states before it learns how to prevent unsafety. In this paper, we propose a safety-aware DRL framework for single-hall data center cooling control. It applies offline imitation learning and online post-hoc rectification to holistically prevent thermal unsafety during online DRL. In particular, the post-hoc rectification searches for the minimum modification to the DRL-recommended action such that the rectified action will not result in unsafety. The rectification is designed based on a thermal state transition model that is fitted using historical safe operation traces and able to extrapolate the transitions to unsafe states explored by DRL. Extensive evaluation for chilled water and direct expansion cooled data centers in two climate conditions shows that our approach saves 18\\% to 26\\% power compared with conventional control, reduces safety violations by 85\\% to 99\\% compared with reward shaping.

• Multi-Objective Controller Synthesis with Uncertain Human Preferences, Shenghui Chen, Kayla Boggess, David Parker, Lu Feng (The University of Texas at Austin, University of Virginia, University of Birmingham)
  • pre-recorded video (password protected)

  Abstract

  Multi-Objective Controller Synthesis with Uncertain Human Preferences

  • Shenghui Chen, The University of Texas at Austin
  • Kayla Boggess, University of Virginia
  • David Parker, University of Birmingham
  • Lu Feng, University of Virginia

  Complex real-world applications of cyber-physical systems give rise to the need for multi-objective controller synthesis, which concerns the problem of computing an optimal controller subject to multiple (possibly conflicting) criteria. The relative importance of objectives is often specified by human decision-makers. However, there is inherent uncertainty in human preferences (e.g., due to artifacts resulting from different preference elicitation methods). In this paper, we formalize the notion of uncertain human preferences, and present a novel approach that accounts for this uncertainty in the context of multi-objective controller synthesis for Markov decision processes (MDPs). Our approach is based on mixed-integer linear programming and synthesizes an optimally permissive multi-strategy that satisfies uncertain human preferences with respect to a multi-objective property. Experimental results on a range of large case studies show that the proposed approach is feasible and scalable across varying MDP model sizes and uncertainty levels of human preferences. Evaluation via an online user study also demonstrates the quality and benefits of the synthesized controllers.

• Safe HVAC Control via Batch Reinforcement Learning, Hsin-Yu Liu, Bharathan Balaji, Sicun Gao, Rajesh K. Gupta, Dezhi Hong (UC San Diego)
  • pre-recorded video (password protected)

  Abstract

  Safe HVAC Control via Batch Reinforcement Learning

  • Hsin-Yu Liu, University of California, San Diego
  • Bharathan Balaji, Amazon
  • Sicun Gao, University of California, San Diego
  • Rajesh K. Gupta, University of California, San Diego
  • Dezhi Hong, University of California, San Diego

  Buildings account for 30% of energy use worldwide, and approxi-
  mately half of it is ascribed to HVAC systems. Reinforcement Learn-
  ing (RL) has improved upon traditional control methods in increas-
  ing the energy efficiency of HVAC systems. However, prior works
  use online RL methods that require configuring complex thermal
  simulators to train or use historical data-driven thermal models that
  can take at least 10^4 time steps to reach rule-based performance
  Also, due to the distribution drift from simulator to real buildings,
  RL solutions are therefore seldom deployed in the real world. On
  the other hand, batch RL methods can learn from the historical
  data and improve upon the existing policy without any interactions
  with the real buildings or simulators during the training. With the
  existing rule-based policy as the priors, the policies learned with
  batch RL are better than the existing control from the first day of
  deployment with very few training steps compared with online
  methods.
  Our algorithm incorporates a Kullback-Leibler (KL) regulariza-
  tion term to penalize policies that deviate far from the previous
  ones. We evaluate our framework on a real multi-zone, multi-floor
  building—it achieves 7.2% in energy reduction cf. the state-of-the-
  art batch RL method, and outperforms other BRL methods in occu-
  pants’ thermal comfort, and 16.7% energy reduction compared to
  the default rule-based control.

Full program for ICCPS Posters and Demo Session(s) listed [Here]

Full program for ICCPS Posters and Demo Session(s) listed [Here]

Session Chair: Oleg Sokolosky

• Exploring the Performance of Deep Neural Networks on Embedded Many-Core Processors, Takuma Yabe, Azumi Takuya (Saitama University)
  • pre-recorded video (password protected)

  Abstract

  Exploring the Performance of Deep Neural Networks on Embedded Many-Core Processors

  • Takuma Yabe, Saitama University
  • Azumi Takuya, Saitama University

  This paper explores and evaluates the potential of deep neural network (DNN)-based machine learning algorithms on embedded many-core processors in cyber-physical systems, such as self-driving systems. To run applications in embedded systems, a platform characterized by low power consumption with high accuracy and real-time performance is required. Furthermore, a platform is required that allows the coexistence of DNN applications and other applications, including conventional real-time control software, to enable advanced embedded systems, such as self-driving systems. Clustered many-core processors, such as Kalray MPPA3-80 Coolidge, can run multiple applications on a single platform because each cluster can run applications independently. Moreover, MPPA3-80 integrates multiple arithmetic elements that operate at low frequencies, thereby enabling high performance and low power consumption comparable to that of embedded graphics processing units. Furthermore, Kalray Neural Network (KaNN) code generator, a deep learning inference compiler for the MPPA3-80 platform, can efficiently perform DNN inference on MPPA3-80. This paper evaluates DNN models, including You Only Look Once (YOLO)-based and Single Shot MultiBox Detector (SSD)-based models, on MPPA3-80. The evaluation examines the frame rate and power consumption in relation to the size of the input image, the computational accuracy, and the number of clusters.

• VaRSM：Versatile Autonomous Racquet Sports Machine, Fan Yang, Zhiwei Shi, Sixian Ye, Jiazhong Qian, Wenjie Wang, Dong Xuan (Zhejiang DeepCode Robotics, Shandong University)
  • pre-recorded video (password protected)

  Abstract

  VaRSM：Versatile Autonomous Racquet Sports Machine

  • Fan Yang, Zhejiang DeepCode Robotics Co. Ltd.
  • Zhiwei Shi, Zhejiang DeepCode Robotics Co. Ltd.
  • Sixian Ye, Zhejiang DeepCode Robotics Co. Ltd.
  • Jiazhong Qian, Zhejiang DeepCode Robotics Co. Ltd.
  • Wenjie Wang, Zhejiang DeepCode Robotics Co. Ltd.
  • Dong Xuan, Shandong University

  In this paper, we present a system called Versatile Autonomous Racquet Sports Machine (VaRSM in short). VaRSM can play table tennis, tennis and badminton balls with respective rackets. There are two major challenges in building VaRSM; first, VaRSM must be able to strike and return balls of variable speed and power on fields of varied size with various racquet motions; second, because of the balls’ high speed, VaRSM must track and predict their trajecto- ries as well as move its body in extremely short periods of time. To address these challenges, we design several innovative tech- nologies, which can be grouped into the physical hardware module and the control software module. In the physical hardware module, we create a high speed swerve-drive platform and a high-flexibility rac- quet arm, both with configurable “integrated drive units” (IDU). In the control software module, we take full advantage of the ma- chine’s physical abilities and develop a proactive progressive con- trol method to achieve early ball trajectory prediction, quick strik- ing decision making, and fast yet stable mobile platform and racquet arm motion. We build a prototype system based on these technologies. Our experiments demonstrate VaRSM is able to strike and return table tennis, tennis and badminton balls with high success rates and is capable of playing with human players. To our knowledge, VaRSM is the first machine able to play three different ball games. The machine may hold great significance in education, research, economy, and society. Youtube link

• Anomaly based Incident Detection in Large Scale Smart Transportation Systems, Mohammad Jaminur Islam, Jose Paolo Talusan, Shameek Bhattacharjee, Francis Tiausas, Sayyed Mohsen Vazirizade, Abhishek Dubey, Keiichi Yasumoto, Sajal K. Das ( Western Michigan University, NARA Institute of Science and Technology, Vanderbilt University)
  • pre-recorded video (password protected)

  Abstract

  Anomaly based Incident Detection in Large Scale Smart Transportation Systems

  • Mohammad Jaminur Islam, Western Michigan University
  • Jose Paolo Talusan, NARA Institute of Science and Technology
  • Shameek Bhattacharjee, Western Michigan University
  • Francis Tiausas, NARA Institute of Science and Technology
  • Sayyed Mohsen Vazirizade, Vanderbilt University
  • Abhishek Dubey, Vanderbilt University
  • Keiichi Yasumoto, NARA Institute of Science and Technology
  • Sajal K. Das, Missouri University of Science and Technology

  Modern smart cities are focusing on smart transportation solutions to detect and mitigate the effects of various traffic incidents in the city. To materialize this, road side units and ambient transportation sensors are being deployed to collect vehicular data that provides real-time traffic monitoring. In this paper, we first propose a real-time data-driven anomaly-based traffic incident detection framework for a city scale smart transportation system. Specifically, we propose an incremental region growing approximation algorithm for optimal spatio-temporal clustering of road segments and their data; such that road segments are strategically divided into highly correlated clusters. The highly correlated clusters enable identifying a Pythagorean Mean-based invariant as an anomaly detection metric that is highly stable under no incidents but show deviation in the presence of incidents. We learn the bounds of the invariants in a robust manner such that anomaly detection can generalize to unseen events, even when learning from real noisy data. We perform extensive experimental validation using mobility data collected from the City of Nashville, Tennessee, and prove that the method is able to detect incidents within each cluster in real-time.

• Interpretable Detection of Distribution Shifts in Learning Enabled Cyber-Physical Systems, Yahan Yang, Ramneet Kaur, Souradeep Dutta, Insup Lee (University of Pennsylvania)
  • pre-recorded video (password protected)

  Abstract

  Interpretable Detection of Distribution Shifts in Learning Enabled Cyber-Physical Systems

  • Yahan Yang, University of Pennsylvania
  • Ramneet Kaur, University of Pennsylvania
  • Souradeep Dutta, University of Pennsylvania
  • Insup Lee, University of Pennsylvania

  The use of learning based components in cyber-physical systems (CPS) has created a gamut of possible avenues to use high dimensional real world signals generated from sensors like camera and LiDAR. The ability to process such signals can be largely attributed to the adoption of high-capacity function approximators like deep neural networks. However this does not come without its potential perils. The pitfalls arise from possible over-fitting, and subsequent unsafe behavior when exposed to unknown environments. One challenge is that, in high dimensional input spaces it is almost impossible to experience enough training data in the design phase. What is required here, is an efficient way to flag out-of-distribution (OOD) samples that is precise enough to not raise too many false alarms. In addition, the system needs to be able to detect these in a computationally efficient manner at runtime. In this paper, our proposal is to build good representations for in-distribution data. We introduce the idea of a memory bank to store prototypical samples from the input space. We use these memories to compute probability density estimates using kernel density estimation techniques. We evaluate our technique on two challenging scenarios : a self-driving car setting implemented inside the simulator CARLA with image inputs, and an autonomous racing car navigation setting, with LiDAR inputs. In both settings it was observed that a deviation from in-distribution setting can potentially lead to deviation from safe behavior. An added benefit of using training samples as memories to detect out-of-distribution input is that the system is interpretable to a human operator. Explanations of this nature is generally hard to obtain from pure deep learning based alternatives.

Session Chair: Lu Feng

• A Dynamic Obfuscation Framework for Security and Utility, Andrew Wintenberg, Matthew Blischke, Stéphane Lafortune, Necmiye Ozay (University of Michigan, University of California)
  • pre-recorded video (password protected)

  Abstract

  A Dynamic Obfuscation Framework for Security and Utility

  • Andrew Wintenberg, University of Michigan, Ann Arbor
  • Matthew Blischke, University of California, Santa Barbara
  • Stéphane Lafortune, University of Michigan, Ann Arbor
  • Necmiye Ozay, University of Michigan, Ann Arbor

  Obfuscation can be used by dynamic systems to ensure private and secure communication over networks vulnerable to eavesdroppers. Balancing the utility of sending information to intended recipients and privacy by hiding information from unintended recipients presents an interesting challenge. We propose a new framework for obfuscation that includes an inference interface to allow intended recipients to interpret obfuscated information. We model the security of the obfuscation with opacity, a formal notion of plausible deniability. Using techniques from distributed reactive synthesis, we show how to automatically design a privacy-enforcing obfuscator along with the inference interface that is given to intended recipients to use as a “key”. We demonstrate this approach by enforcing privacy while maintaining utility in a contact tracing model.

• T-SYS: Timed-Based System Security for Real-Time Kernels, Brayden McDonald, Frank Mueller (North Carolina State University)
  • pre-recorded video (password protected)

  Abstract

  T-SYS: Timed-Based System Security for Real-Time Kernels

  • Brayden McDonald, North Carolina State University
  • Frank Mueller, North Carolina State University

  The increasing proliferation of cyber-physical systems in a multitude of applications presents a pressing need for effective methods of securing such devices. Many such systems are subject to tight timing constraints, which are poorly suited to traditional security methods due to the large runtime overhead and execution time variation introduced. However, the regular (and well documented) timing specifications of real-time systems open up new avenues with which such systems can be secured. This paper contributes T-SYS, a timed-system method of detecting intrusions into real-time systems via timing anomalies. A prototype implementation of T-SYS is integrated into a commercial real-time operating system (RTOS) in order to demonstrate its feasibility. Further, a compiler-based tool is developed to realize a T-SYS implementation with elastic timing bounds. This tool supports integration of T-SYS protection into applications as well as the RTOS the kernel itself. Results on an ARM hardware platform with benchmark tasks including those drawn from an open-source UAV codebase compare T-SYS with another method of timing-based intrusion detection and assess its effectiveness in terms of detecting attacks as they intrude a system.

• Learning-Based Vulnerability Analysis of Cyber-Physical Systems, Amir Khazraei, Spencer Hallyburton, Qitong Gao, Yu Wang, Miroslav Pajic ( Duke University, University of Florida)
  • pre-recorded video (password protected)

  Abstract

  Learning-Based Vulnerability Analysis of Cyber-Physical Systems

  • Amir Khazraei, Duke University
  • Spencer Hallyburton, Duke University
  • Qitong Gao, Duke University
  • Yu Wang, University of Florida
  • Miroslav Pajic, Duke University

  This work focuses on the use of deep learning for vulnerability analysis of cyber-physical systems (CPS). Specifically, we considera control architecture widely used in CPS, where the low-level control is based on a feedback controller and an observer (e.g., the extended Kalman filter (EKF)), while also employing an anomaly detector. To facilitate analyzing the impact potential sensing attacks could have on systems with general nonlinear dynamics, we develop learning-enabled attack generators capable of designing stealthy attacks that maximally degrade system operation. We show how such problem can be cast within a learning-based grey-box framework where only parts of the runtime information are known to the attacker. We then introduce two methods for generating effective stealthy attacks, based on feed-forward neural networks (FNN) and recurrent neural networks (RNN). Both types of attack-generator models are trained offline, using a cost function that combines the attack impact on the estimation error (and thus control) and the residual signal used for anomaly detection; this enables the trained models to recursively generate effective yet stealthy sensor attacks in real-time while requiring different levels of system information at runtime. The effectiveness of the proposed methods is demonstrated on several case studies with varying levels of complexity and nonlinearity: inverted pendulum, autonomous driving vehicles (ADV), and unmanned areal vehicles (UAVs).

• Protecting Smart Homes from Unintended Application Actions, Aqsa Kashaf, Vyas Sekar, Yuvraj Agarwal (CMU)
  • pre-recorded video (password protected)

  Abstract

  Protecting Smart Homes from Unintended Application Actions

  • Aqsa Kashaf, Carnegie Mellon University
  • Vyas Sekar, Carnegie Mellon University
  • Yuvraj Agarwal, Carnegie Mellon University

  Many smart home frameworks use applications to automate devices in a smart home. When these applications interact in the same environment, they may cause unintended actions which can lead to a safety violation (e.g., the door is unlocked when the user is not at home). While recent efforts have attempted to address this problem, they do not capture complex app behaviors such as: 1) timed behavior and user inputs (e.g., a lock-door app that locks the door after x duration may cause a door to remain unlocked for a long time if $x$ is set too large.) and 2) interactions between devices and the environment they implicitly affect (e.g., water sprinklers cannot be turned on if the water supply is off). Hence, prior work leads to many false positives and false negatives. In this paper, we present PSA, a practical framework to identify safety intent violations in a smart home. PSA uses parameterized timed automata (PTA) as an expressive abstraction to model smart apps. To parse these apps into PTA, we define mappings from smart app APIs to equivalent PTA primitives. We also provide toolkits to model devices, environments, and their interactions. In designing PSA, we identify and tackle key challenges in ensuring correctness of smart home models and discuss trade-offs between their expressiveness and scalability. We evaluate PSA on 86 apps in the Samsung SmartThings IoT ecosystem. We compare PSA against two state-of-the-art baselines and find: (a) 19 new intent violations and (b) 35% fewer false positives than baselines.