Program

Program Overview for CPS-IoT Week 2025

ICCPS Program Overview

Session Location: Emerald Bay B

Time May 7, Wednesday May 8, Thursday May 9, Friday
10:30am-12:00pm Session 1: Human-in-the-loop & Ethics in CPS Session 3: Real-Time Systems Session 6: Electric Vehicles, Smart Grids, Industrial Automation
1:30pm-3:00pm Session 2: Verification and Monitoring for Assurance Session 4: Control Systems and Safety Session 7: Privacy, Trust, Honeypots
3:30pm-5:30pm Poster/Demo Presentations Session 5: Medical CPS Session 8: Robotic and Autonomous Systems

Day 1: May 7TH

10:30 AM – 12:00 PM, Session 1: Human-in-the-loop & Ethics in CPS

Session Chair: Mauricio Castillo-Effen

Can control barrier functions keep automated vehicles safe in live freeway traffic?, George Gunte (Vanderbilt University), Mattew Nice (Vanderbilt University), Matt Bunting (Vanderbilt University), Jonathan Sprinkle (Vanderbilt University) and Daniel Work (Vanderbilt University)

Abstract

This work presents testing of a Control Barrier Function (CBF) supervised Automated Vehicle (AV) in live freeway traffic. The CBF is designed and  implemented using a common dynamical model for AV longitudinal control and a time-gap based safety property combined with CAN bus injection software/hardware. Over an hour of car-following data is collected from driving in congested freeway traffic. We analyze the extent to which the CBF controlled AV satisfied three properties: 1) forward-invariance of the safety property, 2) recovery of the safety property, and 3) collision avoidance.
Our main findings are as follows. Forward-invariance was not strictly satisfied across all states. When trajectories begin satisfying the safety property it was violated by a maximum of 3.4 [m], and 90% of violations were less than 2 [m]. Recovery was also not strictly satisfied across all states. For trajectories which begin outside of the safe set due to merge-in events, if the violation to the safety property was by more than 5 [m] the AV was recovering back to the safe set in more than 98% of the time. Finally, the minimum spacing-gap was 11.7 [m]. Across the tests the AV remained far from any collisions. We additionally analyze errors between control inputs and achieved outputs and hypothesize that unaccounted for modeling errors may lead to under-braking compared to what the CBF logic specifies, which may contribute to the observed property violations.


Breaking the Latency Barrier: Practical Haptic Bilateral Teleoperation over 5G, Herman Kroep (Delft University of Technology), Stijn Coppens (Delft University of Technology), Koen Wösten (Delft University of Technology), Anup Bhattacharjee (Delft University of Technology) and R.R. Venkatesha Prasad (Delft University of Technology)

Abstract

Haptic bilateral teleoperation holds promise for applications such as telemaintenance, remote manipulation, and disaster response, yet delivering precise, low-latency force and video feedback remains challenging. This study advances haptic bilateral teleoperation by combining live video with Model Mediated Teleoperation (MMT) to enable predictive force feedback. A novel algorithm allows the robotic device to replicate interactions predictively experienced by the operator. We validated this approach in a fully functional system that performs reliably despite significant network delays. The latency performance of the system is extensively characterized, achieving a motion-to-pixel latency of 58 ms. A user study revealed that operators did not perceive network latency of at least 75 ms, resulting in a 133 ms motion-to-pixel delay requirement. Additionally, a 5G latency analysis demonstrated that effective haptic teleoperation is achievable with both operator and remote ends connected via 5G. This provides a path away from strict latency requirements toward practical teleoperation solutions using currently available technology.


Ethics by Design in Autonomous Driving: Developing a Model-Based Liability Determination Framework, Yichuan Yu (ShanghaiTech University), Chenyang Mao (ShanghaiTech University) and Zhihao Jiang (ShanghaiTech University)

Abstract

Driving is a safety-critical activity, with most accidents caused by human errors. Advances in artificial intelligence (AI) offer the potential to reduce these errors, yet AI systems still face challenges in making socially acceptable decisions under complex and dynamic circumstances. To overcome these challenges, incorporating ethic-by-design principles is essential in developing autonomous systems. A crucial component of ethic-by-design is liability determination, which remains difficult to automate due to the need for retrospective analysis of vague and subjective criteria. In this paper, we propose a model-based liability determination framework that integrates legal doctrines with a driver behavior model. Our framework first formalizes liability determination based on established legal principles. The driver behavior model enables retrospective analysis by identifying reasonable alternative actions at each decision point, facilitating the assessment of duty breaches and proximate causes. We validate our framework through experiments focusing on highway driving accidents. We selected 8 representative simulated accidents and evaluated them with 5 senior traffic polices. The results demonstrate that our framework’s liability judgments closely align with those of the police, indicating high accuracy. Additionally, we examined the impact of breach of duty judgments on liability determination by utilizing Large Language Models (LLMs). The findings reveal that with only trajectories, LLM’s liability determinations were inaccurate, whereas incorporating these judgments resulted in outputs that matched police assessments. Our proposed liability determination framework effectively automates the process, providing accurate and interpretable results that support ethic-by-design in autonomous driving systems, thereby enhancing their safety and accountability.


1:30 PM – 3:00 PM, Session 2: Verification and Monitoring for Assurance

Session Chair: Giulia Pedrielli

Perception-based Quantitative Runtime Verification for Learning-enabled Cyber-Physical Systems, Ryan Brown (University of Nebraska-Lincoln), Luan Nguyen (University of Dayton), Weiming Xiang (Augusta University), Marilyn Wolf (University of Nebraska-Lincoln) and Hoang-Dung Tran (University of Nebraska-Lincoln)

Abstract

This paper proposes a perception-based quantitative approach to verify the safety of learning-enabled Cyber-Physical Systems (Le-CPS) at runtime. The proposed approach is developed based on probstar reachability, a new quantitative verification method for deep neural networks. It has two main components: perception-based runtime modeling and runtime quantitative verification. The perception-based runtime modeling method uses a probabilistic perception network to estimate the poses (modeled as a multivariate normal distribution) of moving obstacles. We transform sensing, actuating, and perception uncertainties into probabilistic initial conditions for the system’s states. The system model and initial conditions serve as inputs to a runtime reachability analysis algorithm, which constructs the system’s reachable sets for a short future horizon. These reachable sets are then used to quantitatively verify the system’s safety violation probability in real time. Our approach has been successfully deployed and validated on a real learning-based F1Tenth testbed with multiple autonomous driving scenarios, demonstrating its potential for enhancing the safety and reliability of autonomous systems. The reachable sets are used to quantitatively verify the safety violation probability of the system at runtime.


Safety Monitoring for Learning-Enabled Cyber-Physical Systems in Out-of-Distribution Scenarios, Vivian Lin (University of Pennsylvania), Ramneet Kaur (SRI), Yahan Yang (University of Pennsylvania), Souradeep Dutta (University of British Columbia), Yiannis Kantaros (Washington University in St. Louis), Anirban Roy (SRI), Susmit Jha (SRI), Oleg Sokolsky (University of Pennsylvania) and Insup Lee (University of Pennsylvania)

Abstract

The safety of learning-enabled cyber-physical systems is hindered by the well-known vulnerabilities of deep neural networks to out-of-distribution (OOD) inputs. Existing literature has sought to monitor the safety of such systems by detecting OOD data. However, such approaches have limited utility, as the presence of an OOD input does not necessarily imply the violation of a desired safety property. We instead propose to directly monitor safety in a manner that is itself robust to OOD data. To this end, we predict violations of signal temporal logic safety specifications based on predicted future trajectories. Our safety monitor additionally uses a novel combination of adaptive conformal prediction and incremental learning. The former obtains probabilistic prediction guarantees even on OOD data, and the latter prevents overly conservative predictions. We evaluate the efficacy of the proposed approach in two case studies on safety monitoring: 1) predicting collisions of an F1Tenth car with static obstacles, and 2) predicting collisions of a race car with multiple dynamic obstacles. We find that adaptive conformal prediction obtains theoretical guarantees where other uncertainty quantification methods fail to do so. Additionally, combining adaptive conformal prediction and incremental learning for safety monitoring achieves high recall and timeliness while reducing loss in precision. We achieve these results even in OOD settings and outperform alternative methods.


Mining Specifications for Predictive Safety Monitoring, Eleonora Nesterini (TU Wien), Ezio Bartocci (TU Wien), Alessio Gambi (AIT Austrian Institute of Technology), Dejan Nickovic (AIT Austrian Institute of Technology), Sanjit Seshia (University of California Berkeley) and Hazem Torfah (Chalmers University of Technology)

Abstract

Safety-critical autonomous systems must reliably predict unsafe behavior to take timely corrective actions. Safety properties are often defined over variables that are not directly observable at runtime, making prediction and detection of violations hard. We present a new approach for learning interpretable monitors characterized by concise Signal Temporal Logic (STL) formulas that can predict safety property violations from the observable sensor data. We train these monitors from synthetic, possibly highly unbalanced data generated in a simulation environment. Our specification mining procedure combines a grammar-based method and two novel ensemble techniques. Our approach outperforms the existing solutions by enhancing accuracy and explainability, as demonstrated in two autonomous driving case studies.


Scalable and Interpretable Verification of Image-based Neural Network Controllers for Autonomous Vehicles, Aditya Parameshwaran (Clemson University) and Yue Wang (Clemson University)

Abstract

Existing formal verification methods for image-based neural network controllers in autonomous vehicles often struggle with high-dimensional inputs, computational inefficiency, and a lack of explainability. These challenges make it difficult to ensure safety and reliability, as processing high-dimensional image data is computationally intensive and neural networks are typically treated as black boxes. To address these issues, we propose SEVIN (Scalable and Explainable Verification of Image-Based Neural Network Controllers), a framework that leverages a Variational Autoencoders (VAE) to encode high-dimensional images into a lower-dimensional, explainable latent space. By annotating latent variables with corresponding control actions, we generate convex polytopes that serve as structured input spaces for verification, significantly reducing computational complexity and enhancing scalability. Integrating the VAE’s decoder with the neural network controller allows for formal and robustness verification using these explainable polytopes. Our approach also incorporates robustness verification under real-world perturbations by augmenting the dataset and retraining the VAE to capture environmental variations. Experimental results demonstrate that SEVIN achieves efficient and scalable verification while providing explainable insights into controller behavior, bridging the gap between formal verification techniques and practical applications in safety-critical systems.


3:30 PM – 5:30 PM: POSTER/DEMO Session

Verification

  • Poster Abstract: PRoTECT: Parallel Construction of Barrier Certificates for Safety Verification of Polynomial Systems, Ben Wooding, Viacheslav Horbanov and Abolfazl Lavaei
  • Poster Abstract: Physics-Informed Safety Verification of Nonlinear Systems: A Scenario Approach with Data Mitigation, Mohammadhossein Ashoori, Ali Aminzadeh, Abolfazl Lavaei and Amy Nejati
  • Poster Abstract: Verifying Vision-Based Autonomy with Abstract Rendering and Perception Contracts, Yangge Li, Chenxi Ji and Sayan Mitra
  • Poster Abstract: A gray box approach for Large Language Model-guided Natural Language to Temporal Logic Automatic, Eshita Shukla, Quinn Thibeault and Giulia Pedrielli
  • Poster Abstract: Symbolic Gaussian Smoothing, Andrew Mata, Ali Arjomandbigdeli and Stanley Bak
  • Poster Abstract: Polynomial Zonotopes Intersection Checking, Ertai Luo, Yushen Huang, Yifan Sun and Stanley Bak

Detection

  • Demo Abstract: SEQUIN: A Network Science and Physics-based Approach to Identify Sequential N-k Attacks in Electric Power Grids, Andrew Chio, Russell Bent, Kaarthik Sundar and Nalini Venkatasubramanian
  • Poster Abstract: Monitor and Recover: A Paradigm for Future Research on Distribution Shift in Learning-Enabled Cyber-Physical Systems, Vivian Lin and Insup Lee
  • Poster Abstract: Conformance-Driven Anomaly Detection for Cyber-Physical Systems, Xin Qin
  • Poster Abstract: Integrating the Simplex Architecture to Enhance Safety in Deep Learning Autonomous Systems, Niko Salamini, Federico Nesti, Mauro Marinoni, Giorgiomaria Cicero, Gabriele Serra, Alessandro Biondi and Giorgio Buttazzo
  • Demo Abstract: Real-Time Freeway Traffic Anomalous Event Detection System via Radar Detector Sensors, Austin Coursey, Junyi Ji, Zhiyao Zhang, William Barbour, Marcos Quinones-Grueiro, Tyler Derr, Gautam Biswas and Daniel Work
  • Poster Abstract: Data Efficient PV based Indoor Event Detection, Tushar Routh, Jiechao Gao and Bradford Campbell
  • Poster Abstract: Detecting Stealthy False Data Injections on Cyber-Physical Systems using Temporal Distance Metrics, Akash Bhattacharya, Suraj Singh, Sunandan Adhikary and Soumyajit Dey

Simulation

  • Poster Abstract: Adaptive Beamforming for Connected Vehicles – A Co-simulation Framework, Anik Roy, Varuni Reddy, Somnath Hazra, Serene Banerjee, Arnab Sarkar and Soumyajit Dey
  • Poster Abstract: 1000DaySim: Open-Source Traffic Simulation With Real Data Over Long Time Horizons, Zhiyao Zhang, Yuhang Zhang, Marcos Quiñones-Grueiro, William Barbour, Gautam Biswas and Daniel Work
  • Poster Abstract: Reproducible and Low-cost Sim-to-real Environment for Traffic Signal Control, Yiran Zhang, Khoa Vo, Longchao Da, Tiejin Chen, Xiaoou Liu and Hua Wei
  • Poster Abstract: SPHERE CPS: A Reconfigurable Testbed for Industrial Control System Security Experimentation, Luis Garcia, Jelena Mirkovic, David Balenson, Erik Kline, David Choffnes, Daniel Dubois, Srivatsan Ravi, Joseph Barnes, George Pradkin, Geoff Lawler, Chris Tran and Alba Regalado
  • Poster Abstract: Exploring Flexible Road Reconstruction in Godot Simulator, Daniel Peralta and Xin Qin
  • Poster Abstract: High-Level Scenario Management For Parallel Autonomous Vehicle Simulation, Alex Richardson and Jonathan Sprinkle
  • Demo Abstract: Cost-Effective Rover for Farms, Pawan Kumar, Yejur Dube and Hokeun Kim

Day 2: May 8TH

10:30 AM – 12:00 PM, Session 3: Real-Time Systems

Session Chair: TBD

T-Tex: Timed Threaded Execution in Real-Time OpenMP, Swastik Mittal (North Carolina State University) and Frank Mueller (North Carolina State University)

Abstract

Task scheduling and resource management are increasingly subject to attacks exposing system vulnerabilities, particularly on multi-core processors with an attack surface crossing cores and tasks with different privileges. Meanwhile, modern real-time systems utilize multi-core environments, where delay attacks can force misses. This work proposes “Timed Threaded Execution” (T-Tex), a method to detect such security attacks based on monitoring time dilation induced by unexplained delays in general and more specifically for OpenMP. T-Tex extends OpenMP by exposing it to timed monitoring of code execution. It contributes novel compilation techniques for timed instrumentation exemplified for LLVM via multi-phase profiling using OpenMP tracing (OMPT) capabilities. T-Tex also con- tributes Linux kernel modifications to monitor thread-level execution time across context switches between threads. Experiments on a real platform demonstrate that T-Tex can detect 100% of delay-based intrusions constrained by timer granularity to an unprecedented 60us vulnerability threshold at a performance overhead of 11% − 72% for Parsec and daphne benchmarks.


Stealthy Computational Delay Attacks on Control Systems, Talitha Nauta (Lund University), Henrik Sandberg (KTH) and Martina Maggio (Saarland University)

Abstract

Cyber-Physical Systems (CPS) are essential in critical infrastructure, but their interconnected nature makes them vulnerable to cyber attacks that can disrupt physical processes. Traditional defences in CPS often focus on identifying direct manipulations of control signals or measurement data, but are limited in detecting attacks that introduce computational delays to degrade system performance. Under these attacks, the controller task cannot complete at the time a new control signal is needed. This paper presents a novel optimisation framework for modelling and executing stealthy computational delay attacks on discrete-time linear time-invariant closed-loop systems. The calculated attacks evade detection by disrupting the timing of the controller executions only subtly, and only introducing computational delays when they are most effective. We evaluate the framework on two control systems: a stable quadruple-tank system, and an unstable Furuta pendulum. The evaluation demonstrates that even brief undetected delays can lead to system destabilisation. The results emphasise the need for improved detection strategies that account for time-based threats, in addition to standard detection mechanisms that focus on the consistency between observed measurements and control models.


MAARS: Multi-Rate Attack-Aware Randomized Scheduling for Securing Real-time Systems, Arkaprava Sain (Indian Institute of Technology Kharagpur), Sunandan Adhikary (Indian Institute of Technology Kharagpur), Ipsita Koley (Indian Institute of Technology Kharagpur) and Soumyajit Dey (Indian Institute of Technology Kharagpur)

Abstract

Modern Cyber-Physical Systems (CPSs) consist of numerous control units interconnected by communication networks. Each control unit executes multiple safety-critical and non-critical tasks in real-time. Most of the safety-critical tasks are executed with a fixed sampling period to ensure deterministic timing behaviour that helps in its safety and performance analysis. However, adversaries can exploit this deterministic behaviour of periodic safety-critical tasks to launch schedule-based attacks (SBAs) on them. This paper aims to prevent and minimize the possibility of SBAs compromising the control units. This is achieved by switching between strategically chosen periodicities of the safety-critical control tasks to ensure their performance remains unhampered. Thereafter, we present a novel schedule vulnerability analysis methodology to switch between valid schedules generated for these multiple periodicities of the control tasks at run time. Utilizing these strategies, we introduce a novel Multi-Rate Attack-Aware Randomized Scheduling (MAARS) framework for preemptive fixed-priority schedulers that minimize the success rate of timing-inference-based attacks on safety-critical real-time systems. To the best of our knowledge, this is the first work to propose a schedule randomization method with attack awareness that preserves both control theoretic stability and scheduling correctness. We evaluate the efficacy of MAARS in terms of attack prevention on synthetic task sets and an automotive benchmark task set in a Hardware-in-Loop (HiL) environment.


Repairing Control Safety Violations via Scheduler Patch Synthesis, Anand Yeolekar (TCS Research), Supratik Chakraborty (IIT Bombay), Venkatesh R (TCS Research) and Samarjit Chakraborty (UNC Chapel Hill)

Abstract

Cyber-physical systems are typically implemented in software as a set of real-time control tasks. Timing uncertainty at the low-level scheduling layer can lead to deadline misses of control tasks,
that affects control performance and may violate safety properties associated with the high-level control applications. We present a technique to detect and repair control safety violations by synthe-
sizing a scheduler patch – a pre-computed list of jobs to be not scheduled at runtime – that eliminates these violations without the need of modifications at the control or task layer. The technique utilizes a guess–check–repair loop on top of an exact SMT encoding of control and scheduling behaviours, enabling efficient packing of multiple control applications on the execution platform while guaranteeing control safety.


1:30 PM – 3:00 PM, Session 4: Control Systems and Safety

Session Chair: Ivan Ruchkin

Falsification and Control of CPS using the Language Set of Discrete-Time Temporal Logic, Tanmay Khandait (Arizona State University), Christian Abou-Mrad (Oregon State University), Houssam Abbas (Oregon State University) and Giulia Pedrielli (Arizona State University)

Abstract

We present algorithms for Cyber-Physical Systems (CPS) falsification and control, which take advantage of knowing the entire language of the temporal logic specification – that is, the set of signals that satisfy it. In the design of CPS, falsification and control play key roles. Falsification is a testing task, where the goal is to find an input control signal that causes the system’s output trajectory to violate the correctness requirements. Control is the dual: that is, the task of finding a control signal that causes the system’s output to satisfy the specification. When the specification is expressed in a temporal logic, most existing work relies on local optimization heuristics to perform both tasks. Recent work, however, presented a method for computing a representation of the language of a temporal logic formula in (discrete-time) Signal Temporal Logic (STL). In this paper, we explore whether having such a representation offers advantages when performing falsification and control. We introduce new falsification algorithms which combine distance information to the different components of the language to accelerate the convergence to a falsifier. And we introduce a new algorithm for computing a satisfying control signal which works by repeatedly projecting violating output trajectories back onto the language’s components. Despite their relative simplicity, our algorithms demonstrate 10x to 100x speedups relative to the state-of-the-art. Moreover, these algorithms are trivially parallelizable to take advantage of multiple processors.


Uncertainty Quantification for Physics-Informed Traffic Graph Networks, Tianshu Bao (Vanderbilt University), Xiaoou Liu (Arizona State University), Meiyi Ma (Vanderbilt University), Taylor T Johnson (Vanderbilt University) and Hua Wei (Arizona State University)

Abstract

Predicting spatiotemporal patterns is essential for traffic flow forecasting in Intelligent Transportation Systems (ITS), where accurate predictions can greatly enhance traffic management. Currently, data-driven approaches, such as Graph Neural Networks (GNNs) combined with physics-informed partial differential equations (PDEs), have shown promising performance in capturing complex traffic dynamics. However, these models sometimes make unexpected and incorrect predictions with high certainty which will mislead real-world decision-making, particularly in critical scenarios. This lack of uncertainty quantification (UQ), which estimates the confidence of neural networks predictions beyond prediction accuracy, limits the reliability of the predictions. Existing UQ methods in traffic forecasting typically applied to purely data-driven models, leaving the effects of physics-informed approaches on UQ largely unexplored. In this paper, we address these challenges by combining multiple UQ baselines with physics-informed methods to investigate the impact of physical constraints on UQ for traffic forecasting. Additionally, we introduce a new physics-informed loss function to guide the model learning process, which holds an exponential relation and complements the linear relations of the PDE layer. Through extensive experiments on real-world traffic datasets, we demonstrate that our proposed method outperforms existing approaches, achieving reductions of up to 14.8% in short-term and 8.7% in long-term traffic speed prediction errors. Sensitivity analysis further illustrates the robustness of our approach under perturbations.


Human-In-The-Loop Classification of Adaptive Cruise Control at a Freeway Scale, Xia Wang (Vanderbilt University), Matthew Nice (Vanderbilt University), Matt Bunting (Vanderbilt University), Fangyu Wu (University of California, Berkeley), Maria Laura Delle Monache (University of California, Berkeley), Jonathan Lee (University of California, Berkeley), Benedetto Piccoli (Rutgers University-Camden), Benjamin Seibold (Temple University), Alexandre Bayen (University of California, Berkeley), Daniel Work (Vanderbilt University) and Jonathan Sprinkle (Vanderbilt University)

Abstract

The goal of this paper is to estimate whether a human or Adaptive Cruise Control (ACC) is managing a vehicle’s speed control, based on observations by external sensors. The driving characteristics of individual vehicles—whether human-driven or ACC-controlled—play a crucial role in shaping overall traffic flow. To enable advanced traffic control strategies tailored to specific vehicle behaviors, this paper introduces a time-series deep learning classifier that leverages multiple models, including One-Dimensional Convolutional Neural Networks (1D-CNN), Recurrent Neural Networks (RNN), Long Short-Term Memory (LSTM), Gated Recurrent Units (GRU), and Temporal Fusion Transformers (TFT). These models distinguish between human-driven and ACC-controlled trajectories using signals such as the ego vehicle’s velocity, the distance to the leading vehicle, and derived features. Unlike previous studies relying solely on simulation data, our classifier uses large-scale, real-world datasets from field experiments and daily commute data. By utilizing low-latency, low-anomaly signals decoded from Controller Area Network (CAN) bus messages, the model achieves a high accuracy of 98.85\% in classifying human-driven and ACC-controlled vehicles within three seconds, outperforming existing methods that require longer trajectory data or pre-calibrated models. The approach is scalable and can be integrated with large-scale traffic trajectory datasets, such as those from the I-24 Motion project, enabling more precise estimation of ACC penetration, fuel consumption, and emissions.


Certified Inductive Synthesis for Online Mixed-Integer Optimization, Marco Zamponi (IMT School for Advanced Studies Lucca), Emilio Incerto (IMT School for Advanced Studies Lucca), Daniele Masti (GSSI Gran Sasso Science Institute, L’Aquila, Italy) and Mirco Tribastone (IMT School for Advanced Studies Lucca)

Abstract

In fields such as autonomous and safety-critical systems, online optimization plays a crucial role in control and decision-making processes, often requiring the integration of continuous and discrete variables. These tasks are frequently modeled as mixed-integer programming (MIP) problems, where feedback data are incorporated as parameters. However, solving MIPs within strict time constraints is challenging due to their $\mathcal{NP}$-complete nature. A promising solution to this challenge involves leveraging the largely invariant structure of these problems to perform most computations offline, thus enabling efficient online solving even on platforms with limited hardware capabilities. In this paper we present a novel implementation of this strategy that uses counterexample-guided inductive synthesis to split the MIP solution process into two stages. In the offline phase, we construct a mapping that provides feasible assignments for binary variables based on parameter values within a specified range. In the online phase, we solve the remaining continuous part of the problem by fixing the binary variables to the values predicted by this mapping. Our numerical evaluation demonstrates the efficiency and solution quality of this approach compared to standard mixed-integer solvers, highlighting its potential for real-time applications in resource-constrained environments.


3:30 PM – 5:30 PM: Session 5: Medical CPS

Session Chair: Huajie Shao

Psychophysiology-aided Perceptually Fluent Speech Analysis of Children Who Stutter, Yi Xiao (Arizona State unviersity), Harshit Sharma (Arizona State University), Victoria Tumanova (Syracuse University) and Asif Salekin (Arizona State unviersity)

Abstract

This paper presents a novel approach named PASAD that detects changes in perceptually fluent speech acoustics of young children. Particularly, analysis of perceptually fluent speech enables identifying the speech-motor-control factors that are considered as the underlying cause of stuttering disfluencies. Recent studies indicate that the speech production of young children, especially those who stutter, may get adversely affected by situational physiological arousal. A major contribution of this paper is leveraging the speaker’s situational physiological responses in real-time to analyze the speech signal effectively. The presented PASAD approach adapts a Hyper-Network structure to extract temporal speech importance information leveraging physiological parameters. Moreover, we collected speech and physiological sensing data from 73 preschool-age children who stutter (CWS) and who don’t stutter (CWNS) in different conditions. PASAD’s unique architecture enables identifying speech attributes distinct to a CWS’s fluent speech and mapping them to the speaker’s respective speech-motor-control factors. Extracted knowledge can enhance understanding of children’s speech-motor-control and stuttering development. Our comprehensive evaluation shows that PASAD outperforms state-of-the-art multi-modal baseline approaches in different conditions, is expressive and adaptive to the speaker’s speech and physiology, generalizable, robust, and is real-time executable.


EXACT: A Meta-Learning Framework for Precise Exercise Segmentation in Physical Therapy, Hanchen David Wang (Vanderbilt University), Siwoo Bae (Vanderbilt University), Xutong Sun (Vanderbilt University), Yashvitha Thatigotla (Vanderbilt University) and Meiyi Ma (Vanderbilt University)

Abstract

Wearable sensor technology has significantly enhanced healthcare quality, including physical therapy. However, due to the design of current deep learning models, existing works often ignore the unique variations of rest intervals between repetitions and variations in individual user progress, potentially hindering effective therapy outcomes. To address these limitations, we introduce EXACT, a novel framework designed to improve exercise segmentation and differentiate between exercise variations and rest intervals in PT applications. EXACT leverages a unique combination of a U-Net architecture integrated with Model-Agnostic Meta-Learning (MAML), enhanced with residual connections and attention mechanisms to capture subtle variations in exercise patterns and rest intervals. This approach addresses key challenges in segmenting dense, multivariate IMU data, providing a robust solution that adapts to new tasks with minimal retraining. EXACT achieves up to 20% improvement in segmentation Dice score over state-of-the-art U-Net models, demonstrating superior performance in distinguishing queried exercises from other exercises and rest intervals and handling variability in patient movements. Through rigorous evaluation and ablation studies, we demonstrate that attention and residual connections are essential for propagating relevant feature information and maintaining generalizability across varied exercise contexts. EXACT’s adaptability and precision make it a valuable tool for real-time monitoring in PT, offering enhanced insights into patient progress and exercise quality in rehabilitation tracking.


JOIN: Optimized Light Source Activation for Deep Tissue Optical Sensing, Kourosh Vali (University of California Davis), Begum Kasap (University of California Davis), Ata Vafi (University of California Davis) and Soheil Ghiasi (University of California Davis)

Abstract

In wearable optical sensing systems, non-idealities present during measurement affect the quality of acquired signals of interest. The issue is of particular significance in deep tissue sensing applications in which, the signal of interest is faint relative to typical noise sources that contaminate the measured data. To mitigate the problem, we investigate the role of optimizing light source activation pulse, specifically its toggling rate and duty cycle. We identify the potential for the optical source activation signal to mitigate the problem and characterize its design space. Subsequently, we present JOIN, an algorithm that yields the parameters of an optimized activation signal for a given profile of contextual noise profile. Through this algorithm, we strike a balance between avoiding noisy spectral regions associated with environmental disturbances and fitting a judiciously-selected number of signal harmonics into the measurement bandwidth, thereby enhancing the signal-to-noise ratio (SNR) of the acquired data from deep tissue by as much as 6dB. The proposed method is validated through analytical derivations, as well as test bench and in-vivo measurements on human subjects.


Day 3: May 9TH

10:30 AM – 12:00 PM, Session 6: Electric Vehicles, Smart Grids, Industrial Automation

Session Chair: TBD

eFlx: Energy Flexibility Provisioning for E-Taxi Fleets, Liangkai Zhou (Stony Brook University), Yue Zhao (Stony Brook University), Yukun Yuan (University of Tennessee at Chattanooga), Ce Xu (Stony Brook University) and Shan Lin (Stony Brook University)

Abstract

An e-taxi fleet consumes a significant amount of energy daily, making it a substantial electricity consumer. Different from traditional consumers, e.g., factories and buildings, a fleet coordinates charging activities across both times and locations, offering considerable flexibility in its energy demand. This allows a fleet to achieve substantial reductions in energy consumption in response to demand response requests, while maintaining transportation service quality. To better understand and control this intrinsic energy flexibility, we propose the eFlx framework for managing e-taxi fleets for demand response. In the eFlx framework, we establish a model to characterize the energy flexibility upon receiving a real-time demand response request. We formulate the energy flexibility provisioning problem – a bi-level optimal control problem aimed at optimizing and maintaining the energy flexibility of the fleet for potential demand response requests that could arise at any time. To achieve real-time flexibility provisioning, we develop an efficient iterative algorithm to solve this problem. Extensive data-driven evaluations demonstrate that eFlx achieves 19.98% more energy demand reduction than existing solutions without any need for extra charging or any compromise in taxi service quality.


Online Decision-Making Under Uncertainty for Vehicle-to-Building Systems, Rishav Sen (Vanderbilt University), Yunuo Zhang (Vanderbilt University), Fangqi Liu (Vanderbilt University), Jose Paolo Talusan (Vanderbilt University), Ava Pettet (Nissan Advanced Technical Center Silicon Valley), Yoshinori Suzue (Nissan Advanced Technical Center), Ayan Mukhopadhyay (Vanderbilt University) and Abhishek Dubey (Vanderbilt University)

Abstract

Vehicle-to-building (V2B) systems combine physical infrastructure such as smart buildings and electric vehicles (EVs) connected to chargers at the building, with digital control mechanisms to manage energy use. By utilizing EVs as flexible energy reservoirs, buildings can dynamically charge and discharge EVs to effectively manage energy usage, and reduce costs under time-variable pricing and demand charge policies. This setup leads to the V2B optimization problem, where buildings coordinate EV charging and discharging to minimize total electricity costs while meeting users’ charging requirements. However, the V2B optimization problem is difficult due to: 1) fluctuating electricity pricing, which includes both energy charges (\$/kWh) and demand charges (\$/kW); 2) long planning horizons (usually over 30 days); 3) heterogeneous chargers with differing charging rates, controllability, and directionality (unidirectional or bidirectional); and 4) user-specific battery levels at departure to ensure user requirements are met. While existing approaches often model this setting as a single-shot combinatorial optimization problem, we highlight critical limitations in prior work and instead model the V2B optimization problem as a Markov decision process, i.e., a stochastic control process. Solving the resulting MDP is challenging due to the large state and action spaces. To address the challenges of the large state space, we leverage online search, and we counter the action space by using domain-specific heuristics to prune unpromising actions. We validate our approach in collaboration with an EV manufacturer and a smart building operator in California, United States, showing that the proposed framework significantly outperforms state-of-the-art methods.


SEQUIN: A Network Science and Physics-based Approach to Identify Sequential N-k Attacks in Electric Power Grids, Andrew Chio (University of California, Irvine), Russell Bent (Los Alamos National Laboratory), Kaarthik Sundar (Los Alamos National Laboratory) and Nalini Venkatasubramanian (University of California, Irvine)

Abstract

The electric grid is a vital infrastructure that supplies power on which modern cities and communities depend, and maintaining its reliable service and resilient operation is essential. Recently, extreme events such as natural disasters and man-made attacks have revealed the fragility of the grid, and the widespread consequences that people can face as a result. In general, the grid’s performance relies on a few key components. However, efficiently finding these components is challenging, due to the geo-distributed scale of the grid, complex physics governing power flows, and automated network response. Realistically, identifying these key components must also consider the temporal aspect of how failures affect the network. In this paper, we address the problem of identifying worst-case disruptions to the grid, under the sequential failure of components. We present SEQUIN, a framework leveraging network science principles and physics-based constraint optimization to explore such failures in the grid. We formulate the problem using a sequential N-k interdiction model, which provides a methodology to explore and capture interactions between the failures and network response. Our approach defines several network properties to assess the contribution of each component towards its operation, and provides an efficient guided exploration of attacks. We also provide a toolkit to help reason about the impact on the grid. Extensive experiments on multiple benchmark grid networks are conducted, which demonstrate that the efficacy of our approach, and demonstrate how the ordering of attacks can result in different levels of disruption.


Pay Attention to Network: Reliability-aware Spatial-Temporal-Frequential Scheduling for TSN-WiFi Networks, Miao Guo (Zhejiang University), Yichuan Yang (Zhejiang University), Shibo He (Zhejiang University), Jianping Pan (University of Victoria), Chaojie Gu (Zhejiang University) and Jiming Chen (Zhejiang University)

Abstract

Time-Sensitive Networking (TSN) is a pivotal technology to provide deterministic and reliable communications in wired domain. Complementarily, Wi-Fi Multi-link Operation (MLO) extends the TSN capabilities over wireless domain to further increase the throughput and reliability for wired-wireless-integrated scenarios such as smart factories in industrial automation. To incorporate TSN and Wi-Fi MLO seamlessly, cross-domain flow scheduling is of vital importance in reliable control message transmission. Existing approaches leverage Deep Reinforcement Learning (DRL) to adapt to the dynamic wireless channel quality. However, the traditional multilayer perception (MLP)-based DRL model fails to integrate the input features of all the flows, resulting in severe underfitting issues and scheduling ineffectiveness. In this paper, we observe that the mutual dependencies among flows over the network resource is analogical to the contextual dependencies of tokens over the lexical sequence. Leveraging this insight, we exploit the self-attention mechanism in Natural Language Processing (NLP) to learn the network-wise dependencies among different flows. Theoretically, to provide analytical guide to TSN-WiFi flow scheduling, we present a global scheduling abstraction to describe the key resource constraints of the cross-domain flow scheduling problem. Following that, we propose the load-aware TSN scheduling algorithm and the attention-based DRL scheduling algorithm to allocate spatial-temporal-frequencial resources for flows adhering to the above constraints. Experiments in various settings validate the effectiveness of the proposed method, which enhances the reliability by 12.09% compared with the SOTA method.


1:30 PM – 3:00 PM: Session 7: Privacy, Trust, Honeypots

Session Chair: Xugui Zhou

PLCpot: Application Dialogue Replay based Scalable PLC Honeypot for Industrial Control Systems, Syed Ali Qasim (Grand Valley State University), Taqi Raza (UMass Amherst) and Irfan Ahmed (Virginia Commonwealth University)

Abstract

Programmable Logic Controllers (PLCs) are essential components of industrial control systems (ICS), overseeing critical processes like manufacturing and power generation. As cyberattacks grow
in sophistication, the security community uses PLC honeypots to gather threat intelligence on attackers’ tools and strategies. Existing PLC honeypots, whether low or high interaction, often face challenges in maintaining realism or supporting complex interactions. This paper presents PLCpot, a protocol-agnostic and scalable PLC honeypot framework designed to emulate PLC communication by
analyzing and replaying network traffic. By identifying dynamic fields and function codes within protocols and mapping them to application-level operations, PLCpot supports features such as control logic transfer, basic authentication, and operational modes to enhance attacker engagement.
We demonstrate PLCpot’s emulation capabilities with multiple PLC types, evaluating its potential to replicate common functional and operational behaviors. Additionally, a case study involving
a lab-based elevator model showcases PLCpot’s ability to engage attackers and capture data for analysis. While PLCpot currently supports basic ICS protocols over the transport layer, this framework advances ICS threat intelligence by providing a versatile and scalable approach for emulating PLC behavior and collecting attack data to inform future security measures.


Atlas: Ensuring Accuracy for Privacy-Preserving Federated IoT Applications, Jiechao Gao (University of Virginia), Mingyue Tang (University of Illinois Urbana-Champaign), Wenpeng Wang (University of Virginia), Tushar Routh (University of Virginia) and Brad Campbell (University of Virginia)

Abstract

In smart Internet of Things (IoT) applications, edge devices often collect and store limited data, which is insufficient for training modern deep learning models. Collaborative training methods like cloud computing and federated learning enable robust models for IoT applications, yet introduce data privacy concerns due to central data collection and model inversion attacks. Remedies such as differential privacy can bring data privacy protection but dramatically degrade the accuracy performance of IoT applications. To safeguard user data privacy while maintaining application quality, it is imperative to establish a framework capable of preserving user privacy without compromising accuracy standards.

In this paper, we present Atlas, a private and accurate personalized federated local differential privacy (LDP) framework for IoT applications. We first design a layer-sharing mechanism called the layer importance mask to separate the local model into global and personalized layers. Second, we design a weighted LDP mechanism and add noise to the global layers before transmitting them to the federated learning framework for aggregation. Third, we combine local personalized layers and aggregated global layers to perform IoT tasks. Our experiments on five real-world IoT application datasets and the CIFAR-10 dataset show that our privacy-preserving approach only sacrifices 2\% to 6\% of accuracy compared to the state-of-the-art non-privacy preserving FL frameworks among various IoT applications and outperforms the current LDP-based FL framework by 8\% to 13\%.


Trust-Based Assured Sensor Fusion in Distributed Aerial Autonomy, R. Spencer Hallyburton (Duke University) and Miroslav Pajic (Duke University)

Abstract

Multi-agent collaboration enhances situational awareness in intelligence, surveillance, and reconnaissance (ISR) missions. Ad hoc networks of unmanned aerial vehicles (UAVs) allow for real-time data sharing, but they face security challenges due to their decentralized nature, making them vulnerable to cyber-physical attacks. This paper introduces a trust-based framework for assured sensor fusion in distributed multi-agent networks, utilizing a hidden Markov model (HMM) to estimate the trustworthiness of agents and their provided information in a decentralized fashion. Trust-informed data fusion prioritizes fusing data from reliable sources, enhancing resilience and accuracy in contested environments. To evaluate assured sensor fusion under attacks on sensing, we present a novel multi-agent aerial dataset built from the Unreal Engine simulator. We demonstrate through case studies improved ISR performance and an ability to detect malicious actors in adversarial settings.


Synthesis of Dynamic Masks for Information-Theoretic Opacity in Stochastic Systems, Sumukha Udupa (University of Florida), Chongyang Shi (University of Florida) and Jie Fu (University of Florida)

Abstract

In this work, we investigate the synthesis of dynamic information releasing mechanisms, referred to as “masks”, to minimize information leakage from a stochastic system to an external observer. Specifically, for a stochastic system, an observer aims to infer whether the final state of the system trajectory belongs to a set of secret states. The dynamic mask seeks to regulate sensor information in order to maximize the observer’s uncertainty about the final state, a property known as final-state opacity. While existing supervisory control literature on dynamic masks primarily addresses qualitative opacity, we propose quantifying opacity in stochastic systems by conditional entropy, which is a measure of information leakage in information security. We then formulate a constrained optimization problem to synthesize a dynamic mask that maximizes final-state opacity under a total cost constraint on masking. To solve this constrained optimal dynamic mask synthesis problem, we develop a novel primal-dual policy gradient method. Additionally, we present a technique for computing the gradient of conditional entropy with respect to the masking policy parameters, leveraging observable operators in hidden Markov models.  To demonstrate the effectiveness of our approach, we apply our method to an illustrative example and a stochastic grid world scenario, showing how our algorithm optimally enforces final-state opacity under cost constraints.


3:30 PM – 5:30 PM, Session 8: Robotic and Autonomous Systems

Session Chair: Oleg Sokolsky

Optimal Integrated Task and Path Planning for Collaborative Multi-Robot Systems, Aman Aryan (Qualcomm India Pvt. Ltd.), Manan Modi (SAP Labs India), Indranil Saha (Indian Institute of Technology Kanpur), Rupak Majumdar (MPI-SWS) and Swarup Mohalik (Ericsson Research, Bangalore)

Abstract

We propose a generic multi-robot planning mechanism that combines an optimal task planner and an optimal path planner to provide a scalable solution for complex multi-robot planning problems. The Integrated planner, through the interaction of the task planner and the path planner, produces optimal collision-free trajectories for the robots. We illustrate our general algorithm on an object pick-and-drop planning problem in a warehouse scenario where a group of robots is entrusted with moving objects from one location to another in the workspace. We solve the task planning problem by reducing it into an SMT-solving problem and employing the highly advanced SMT solver Z3 to solve it. To generate collision-free movement of the robots, we extend the state-of-the-art algorithm Conflict Based Search with Precedence Constraints  with several domain-specific constraints. We evaluate our integrated task and path planner extensively on various instances of the object pick-and-drop planning problem and compare its performance  with a state-of-the-art multi-robot classical planner.
Experimental results demonstrate that our planning mechanism can deal with complex planning problems and outperforms a state-of-the-art classical planner both in terms of computation time and the quality of the generated plan.


RLS3: RL-Based Synthetic Sample Selection to Enhance Spatial Reasoning in Vision-Language Models for Indoor Autonomous Perception, Joshua R. Waite (Iowa State University), Md Zahid Hasan (Iowa State University), Qisai Liu (Iowa State University), Zhanhong Jiang (Iowa State University), Chinmay Hegde (New York University) and Soumik Sarkar (Iowa State University)

Abstract

Vision-language model (VLM) fine-tuning for application-specific visual grounding based on natural language instructions has become one of the most popular approaches for learning-enabled autonomous systems. However, such fine-tuning relies heavily on high-quality datasets to achieve successful performance in various downstream tasks. Additionally, VLMs often encounter limitations due to insufficient and imbalanced fine-tuning data. To address these issues, we propose a new generalizable framework to improve VLM fine-tuning by integrating it with a reinforcement learning (RL) agent. Our method utilizes the RL agent to manipulate objects within an indoor setting to create synthetic data for fine-tuning to address certain vulnerabilities of the VLM. Specifically, we use the performance of the VLM to provide feedback to the RL agent to generate informative data that efficiently fine-tune the VLM over the targeted task (e.g. spatial reasoning). The key contribution of this work is developing a framework where the RL agent serves as an informative data sampling tool and assists the VLM in order to enhance performance and address task-specific vulnerabilities. By targeting the data sampling process to address the weaknesses of the VLM, we can effectively train a more context-aware model. In addition, generating synthetic data allows us to have precise control over each scene and generate granular ground truth captions. Our results show that the proposed data generation approach improves the spatial reasoning performance of VLMs, which demonstrates the benefits of using RL-guided data generation in vision-language tasks.


Accelerating Neural Policy Repair with Preservation via Stability-Plasticity Interpolation, Pengyuan Lu (University of Pennsylvania), Oleg Sokolsky (University of Pennsylvania), Insup Lee (University of Pennsylvania) and Ivan Ruchkin (University of Florida)

Abstract

Neural network (NN)-based control policies have been widely adopted in cyber-physical systems (CPS). When a NN-based policy fail to fulfill a formally specified task, researchers leverage NN repair algorithms to fix it. A recent literature raises the problem of Repair with Preservation (RwP), which asks for preservation of existing correct behaviors while repairing the incorrect ones — a corresponding solution is given, known as Incremental Simulated Annealing Repair (ISAR). In this paper, we tackle the computational efficiency issue of ISAR, which involves expensive log-barriered objective functions and wastes computational efforts rolling back when a repaired NN breaks correct behaviors. With our analysis, we reduce the RwP problem to a stability-plasticity (S-P) trade-off interpolation problem, which has been studied in continual learning (CL). Then, we propose our method, ISAR with Interpolation (ISAR-I), which majorly improves ISAR. ISAR-I abandons the expensive log barriers and rolling back to allow intermediate policies to compromise correct behaviors for repair. Then, an interpolation of the S-P trade-off between the original NN and the intermediate NN is kicked off in the Bayesian space, searching for a final NN that both repairs and preserves. Case studies on OpenAI Gym mountain car and an unmanned underwater vehicle show that ISAR-I is able to preserve all verified trajectories while repairing 81.7\% and 21.3\% of the broken ones, respectively, achieving the same performance as ISAR, with runtime cost of only 6.5\% and 19.6\%, on average.