CPS-IOT WEEK 2025: CYBER-PHYSICAL SYSTEMS AND INTERNET-OF-THINGS WEEK
PROGRAM FOR FRIDAY, MAY 9TH
Days:
previous day
all days

View: session overviewtalk overview

07:30-09:00 Breakfast and Registration

Breakfast and Registration

Location: Pacific Room
09:00-10:00 Keynote2: Towards a Design Flow for Verified AI-Based Autonomy

Speaker: Professor Sanjit A. Seshia, University of California, Berkeley, USA

Abstract: Verified artificial intelligence (AI) is the goal of designing AI systems that have strong, ideally provable, assurances of correctness with respect to formally-specified requirements. This talk will review the main challenges to achieving Verified AI, and the progress the research community has made towards this goal. A particular focus will be on AI-based autonomous and semi-autonomous cyber-physical systems (CPS), and on the role of environment/world modeling throughout the design cycle. We argue for developing a new generation of design automation techniques, rooted in formal methods, to enable and support the routine development of high assurance AI-based autonomy. I will describe our work on formal methods for Verified AI-based autonomy, implemented in the open-source Scenic and VerifAI toolkits. The use of these tools will be demonstrated in industrial case studies involving deep learning-based autonomy in ground and air vehicles. We conclude with an outlook to the future of the Verified AI agenda.

Bio: Sanjit A. Seshia is the Cadence Founders Chair Professor in the Department of Electrical Engineering and Computer Sciences (EECS) at the University of California, Berkeley. His research interests are in formal methods for dependable and secure computing, spanning the areas of cyber-physical systems (CPS), computer security, distributed systems, artificial intelligence (AI), machine learning, and robotics. He is co-author of a widely-used textbook on embedded, cyber-physical systems and has led the development of technologies for cyber-physical systems education based on formal methods. His awards and honors include a Presidential Early Career Award for Scientists and Engineers (PECASE), an Alfred P. Sloan Research Fellowship, the Frederick Emmons Terman Award for contributions to EECS education, the IEEE TCCPS Mid-Career Award, a Distinguished Alumnus Award from IIT Bombay, and the Computer-Aided Verification (CAV) Award for contributions to the foundations of SMT solving. He is a Fellow of the ACM and the IEEE.

10:30-12:00

Technical Sessions for all conferences.

10:30-12:00 Session S6 - HSCC: Learning and Optimization for Safe Control
Location: Emerald Bay A
10:30
Extracting Forward Invariant Sets from Neural Network-Based Control Barrier Functions

ABSTRACT. Training Neural Networks (NNs) to serve as Barrier Functions (BFs) is a popular way to improve the safety of autonomous dynamical systems. Despite significant practical success, these methods are not generally guaranteed to produce true BFs in a provable sense, which undermines their intended use as safety certificates. In this paper, we consider the problem of formally certifying a learned NN as a BF with respect to state avoidance for an autonomous system: viz. computing a region of the state space on which the candidate NN is provably a BF. In particular, we propose a sound algorithm that efficiently produces such a certificate set for a shallow NN. Our algorithm combines two novel approaches: it first uses NN reachability tools to identify a subset of states for which the output of the NN does not increase along system trajectories; then, it uses a novel enumeration algorithm for hyperplane arrangements to find the intersection of the NN's zero-sub-level set with the first set of states. In this way, our algorithm soundly finds a subset of states on which the NN is certified as a BF. We further demonstrate the effectiveness of our algorithm at certifying for real-world NNs as BFs in two case studies. We complemented these with scalability experiments that demonstrate the efficiency of our algorithm.

10:55
A learning-based approach to stochastic optimal control under reach-avoid constraint

ABSTRACT. We develop a model-free approach to optimally control stochastic, Markovian systems subject to a reach-avoid constraint. Specifically, the state trajectory must remain within a safe set while reaching a target set within a finite time horizon. Due to the time-dependent nature of these constraints, we show that, in general, the optimal policy for this constrained stochastic control problem is non-Markovian, which increases the computational complexity. To address this challenge, we apply the state-augmentation technique from \cite{schmid2024joint}, reformulating the problem as a constrained Markov decision process (CMDP) on an extended state space. This transformation allows us to search for a Markovian policy, avoiding the complexity of non-Markovian policies. To learn the optimal policy without a system model, and using only trajectory data, we develop a log-barrier policy gradient approach. We prove that under suitable assumptions, the policy parameters converge to the optimal parameters, while ensuring that the system trajectories satisfy the stochastic reach-avoid constraint with high probability.

11:20
Inverse-Optimal Safety Control for Hybrid Systems

ABSTRACT. In this paper, we study control design methods to endow hybrid systems under disturbances with safety guarantees as an inverse-optimality problem. Given an uncertified nominal control law, a safeguarding control law is designed based on a control barrier function to guarantee safety of a set of interest. Due to the myopicproperty of the traditional QP implementation of control barrier functions, an alternative non-QP safety filter is proposed with its corresponding inverse-optimal cost computation in the min-max sense with respect to disturbances. The main results are illustrated in an example.

11:45
TRUST: StabiliTy and Safety ContRoller Synthesis for Unknown Dynamical Models Using a Single Trajectory

ABSTRACT. TRUST is an open-source software tool developed for data-driven controller synthesis of dynamical systems with unknown mathematical models, ensuring either stability or safety properties. By collecting only a single input-state trajectory from the unknown system and satisfying a rank condition that ensures the system is persistently excited according to the Willems et al.'s fundamental lemma, TRUST aims to design either control Lyapunov functions (CLF) or control barrier certificates (CBC), along with their corresponding stability or safety controllers. The tool implements sum-of-squares (SOS) optimization programs solely based on data to enforce stability or safety properties across four system classes: (i) continuous-time nonlinear polynomial systems, (ii) continuous-time linear systems, (iii) discrete-time nonlinear polynomial systems, and (iv) discrete-time linear systems. TRUST is a Python-based web application featuring an intuitive, reactive graphic user interface (GUI) built with web technologies. It can be accessed at URL or installed locally, and supports both manual data entry and data file uploads. Leveraging the power of the Python backend and a JavaScript frontend, TRUST is designed to be highly user-friendly and accessible across desktop, laptop, tablet, and mobile devices. We apply TRUST to a set of physical benchmarks with unknown dynamics, ensuring either stability or safety properties across the four supported classes of models.

10:30-12:00 Session S6 - ICCPS: Electric Vehicles, Smart Grids, Industrial Automation
Chair:
Location: Emerald Bay B
10:30
eFlx: Energy Flexibility Provisioning for E-taxi Fleets

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.

10:52
Online Decision-Making Under Uncertainty for Vehicle-to-Building Systems

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.

11:14
SEQUIN: A Network Science and Physics-based Approach to Identify Sequential N-k Attacks in Electric Power Grids

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.

11:36
Pay Attention to Network: Reliability-Aware Spatial-Temporal-Frequential Scheduling for TSN-WiFi Networks

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.

10:30-12:00 Session S6 - RTAS: Testing and Evaluation
Location: Emerald Bay CDE
10:30
Handling System Overloads: An Empirical Evaluation of Deadline-Miss Handling Strategies

ABSTRACT. In this paper, we present our findings on the evaluation of an overload-resistant control system. We implemented the control of a rotational pendulum on a microcontroller with a state-of-the-art real-time operating system. To mitigate overload conditions, we employed deadline-miss handling strategies that determine how to proceed when a control task exceeds its deadline. The system can either terminate the current controller job (Kill), complete the current job while skipping the next one (Skip-Next), or queue job executions (Queue). We show that the effectiveness of deadline-miss-strategies is highly parameter sensitive. Even subtle and initially unnoticed differences in system assumptions can lead to significant variations in system behavior. Our research thus highlights the importance of evaluation on complete system implementations. Not only did our initial, straightforward implementation perform well under overload conditions, adding deadline-miss handling strategies advocated in related work has proven to be potentially detrimental to the behavior of the pendulum. Based on our initial system implementation, we present and analyze a novel strategy called Shift-On-Miss.

10:52
Arm DynamIQ Shared Unit and Real-Time: An Empirical Evaluation

ABSTRACT. The increasing complexity of embedded hardware platforms poses significant challenges for real-time workloads. Architectural features such as Intel's RDT, Arm QoS, and Arm MPAM are either unavailable on commercial embedded platforms or designed primarily for server environments optimized for average-case performance and might fail to deliver the expected real-time guarantees. Arm DynamIQ Shared Unit (DSU) includes isolation features---among others, hardware per-way cache partitioning---that can improve the real-time guarantees of complex embedded multicore systems and facilitate real-time analysis. However, the DSU also targets average cases, and its real-time capabilities have not yet been evaluated. This paper presents the first comprehensive analysis of three real-world deployments of the Arm DSU on Rockchip RK3568, Rockchip RK3588, and NVIDIA Orin platforms. We integrate support for the DSU at the operating system and hypervisor level and conduct a large-scale evaluation using both synthetic and real-world benchmarks with varying types and intensities of interference. Our results make extensive use of performance counters and indicate that, although effective, the quality of partitioning and isolation provided by the DSU depends on the type and intensity of the interfering workloads. In addition, we uncover and analyze in detail the correlation between benchmarks and different types and intensities of interference.

11:14
LiME: The Linux Real-Time Task Model Extractor

ABSTRACT. We present LiME, a novel dynamic real-time task model extractor. LiME observes the temporal behavior of Linux real-time threads and automatically map the observed activity to established real-time task models: sporadic tasks, periodic tasks, upper and lower arrival curves, cumulative execution-time curves, and two self-suspension models (dynamic and segmented). LiME runs on unmodified Linux kernels and can be used without specialized knowledge of either real-time theory or Linux internals. An extensive evaluation shows LiME to achieve very high inference accuracy---in particular 100% accuracy for common automotive periods---with low kernel overhead, low latency impact, and moderate processor utilization (at best-effort priority).

11:36
ConvolutionalFixedSum: Uniformly Generating Random Values with a Fixed Sum Subject to Arbitrary Constraints

ABSTRACT. This paper addresses the problem of uniform random generation of vectors of values with a fixed sum, subject to upper and lower constraints on the individual component values. Solutions to this problem are used extensively in the generation of tasksets, specifically task utilization values, in support of the performance assessment of schedulability tests for real-time systems. This paper introduces a general-purpose solution in the form of an Inverse Volume Ratio Sampling method that is applicable provided that it is possible to determine the ratio of the volume below a given hyperplane to the total volume of the valid region in n-dimensional space, as demarcated by the constraints and the fixed sum. An efficient approach is derived for volume calculation using numerical convolution, thus instantiating the ConvolutionalFixedSum algorithm, which provides a user-specified level of precision, while scaling at O(n3, log(n)). A stringent uniformity test is developed, called the slices test, which is able to fully explore the extent of the valid region in each of the $n$ dimensions. The slices test reveals that while the outputs of UUnifast and ConvolutionalFixedSum form uniform distributions, in some cases the outputs of prior state-of-the-art algorithms do not.

10:30-12:00 Session S6 - SenSys: Edge AI, Neural Models, & Optimization
10:30
Responsive DNN Adaptation for Video Analytics against Environment Shift via Hierarchical Mobile-Cloud Collaborations

ABSTRACT. Mobile video analysis systems often encounter various deploying environments, where environment shifts present greater demands for responsiveness in adaptations of deployed ``expert DNN models''. Existing model adaptation frameworks primarily operate in a cloud-centric way, exhibiting degraded performance during adaptation and delayed reactions to environment shifts. Instead, this paper proposes MOCHA, a novel framework optimizing the responsiveness of continuous model adaptation through hierarchical collaborations between mobile and cloud resources. Specifically, MOCHA (1) reduces adaptation response delays by performing on-device model reuse and fast fine-tuning before requesting cloud model retrieval and end-to-end retraining; (2) accelerates history expert model retrieval by organizing them into a structured taxonomy utilizing domain semantics analyzed by a cloud foundation model as indices; (3) enables efficient local model reuse by maintaining onboard expert model caches for frequent scenes, which proactively prefetch model weights from the cloud model database. Extensive evaluations with real-world videos on three DNN tasks show MOCHA improves the model accuracy during adaptation by up to 6.8% while saving the response delay and retraining time by up to 35.5x and 3.0x respectively.

10:45
JumpQ: Stochastic Scheduling to Accelerating Object-detection-driven Mobile Sensing on Object-sparse Video Data

ABSTRACT. Deep learning-based object detection has seen a surge in application for sensing systems on mobile devices. In this context, objects are identified and tracked across video frames, facilitating the calculation of associated events of interest. A significant research challenge refers to the acceleration of processing speed, which is constrained by deep learningbased object detection due to its intensive resource requirements. This paper focuses on a typical mobile sensing scenario, wherein sequences of frames containing objects of interest are sparsely dispersed throughout the video stream. Given that many of the frames lack objects, allocating substantial computational resources to detect them becomes inefficient. In light of this, we propose a stochastic scheduling algorithm, JumpQ. JumpQ performs per-frame detection when anticipating the presence of objects in the current frames. Consecutive negative detections prompt a transition to intermittent detection with a probability that undergoes further decay if the negative detection persists until reaching a predefined limit. Upon a positive detection, JumpQ swiftly reverts to per-frame detection and retraces a specific number of previously buffered frames to ensure the inclusion of potentially missed true frames. A comprehensive experimental study using the garbage bag counting technique was conducted to show the efficiency of JumpQ in accelerating the processing speed by nearly 1.92 times while maintaining a negligible impact on sensing accuracy.

11:00
Stochastic Differential Equation Networks for Time Series at Edge

ABSTRACT. Stochastic differential equation networks (SDENets), a subset of continuous-time neural networks, offer the natural ability to model continuous time-series data with greater expressivity than discrete-time neural networks. However, SDENets face challenges related to stability and high computational overhead. In this paper, we introduce SE-SDENet, a stable and efficient variant of SDENet. Leveraging the inherent capability of SDENets to model randomness in time-series data, we establish a theoretical framework that ensures SE-SDENet’s stability during training by regulating the dynamics of each neuron. Additionally, we propose an efficient training and inference framework that enables SE-SDENet to achieve low forward-pass complexity and to dynamically adjust its complexity at run-time. Evaluation with four datasets and four edge devices demonstrates that SE-SDENet achieves a 6.6x higher throughput than the solver-based SDENet and exhibits improved stability in handling noisy data and long-term predictions. A validation on a robot vehicle shows that SE-SDENet can dynamically adjust its complexity at run-time to meet varying resource constraints.

11:15
Lupe: Integrating the Top-down Approach with DNN Execution on Ultra-Low-Power Devices

ABSTRACT. Executing deep neural networks (DNNs) on ultra-low-power (ULP) microcontrollers creates enormous opportunities for new intelligent edge applications. However, manually writing optimized DNN programs for ULP devices is time-consuming and error prone due to the difficulty of managing on-device accelerators. Many prior works address this problem by creating special libraries that tailor common DNN building blocks for unique accelerators of ULP devices. This is a bottom-up approach, as developers build DNNs by assembling library calls. Unfortunately, the encapsulation overhead inherent in this approach greatly reduces accelerator utilization and overall performance. Instead, we advocate for a top-down approach.

We present Lupe, a code generation framework that converts high-level DNN algorithm descriptions to ULP-optimized code. Lupe provides top-down intermittent support that significantly reduces overhead while maintaining intermittent safety. We demonstrate Lupe's benefits on an MSP430, achieving 12.36× and 2.22× average speedup over two prior works across a variety of DNN models in continuous power. Moreover, Lupe reduces the average intermittent runtime costs of prior works by 96.65% and 71.15%, respectively.

11:30
Orbis: Redesigning Neural-enhanced Video Streaming for Live Immersive Viewing

ABSTRACT. Emerging live immersive viewing systems require streaming large 360 videos to users via limited wireless bandwidth. Neural-enhanced video streaming offers a promising solution by streaming downscaled videos and enhancing them by client computation. However, prior systems treated video downscaling and enhancement separately, overlaying existing enhancement techniques onto current video infrastructure to accommodate legacy downscaling methods. This supplemental client design has led to spatial information loss and prohibitive model overheads in 360 video streaming systems. This paper presents Orbis, a redesigned, holistic neural-enhanced video streaming framework that integrates complementary downscaling and enhancement for live immersive viewing. Orbis is empowered by an enhancement-driven interleaved downscaling approach, an inpainting-based enhancement model tailored to interleaved data, and a multi-scale tile adaptation scheme that optimizes immersive viewing experience in dynamic environments. Experimental results show that Orbis improves viewing experience by up to 60% and reduces wireless bandwidth by up to 49% compared to the best-performing baseline.

11:45
E3: Early Exiting with Explainable AI for Real-Time and Accurate DNN Inference in Edge-Cloud Systems

ABSTRACT. Edge intelligence applications frequently generate deep learning inference tasks with varying Service Level Objectives (SLO, such as accuracy and real-time requirements). For such tasks, recent progressive inference modes support early exit from different branches to satisfy inference requirements. However, existing edge-cloud progressive neural architectures cannot simultaneously achieve high accuracy and real-time performance for different data features. Therefore, we utilize explainable AI techniques to construct and train a novel progressive neural architecture called E3. E3 can progressively extract the most important features for inference, ensuring higher accuracy at early-exit points, while the less important features in the later stage are highly compressible, thereby reducing edge-cloud transmission overhead. Furthermore, E3 cooperates with online execution control to launch tasks and decide the exit point for each task, ensuring resource utilization and real-time performance, and adapting to bandwidths and deadlines. Experimental results on various edge-cloud platforms, datasets, and reference models demonstrate that E3 is more lightweight, efficient, energy-saving, and incurs almost no additional runtime overhead compared to traditional architectures. Under stringent deadlines, the average accuracy of tasks increases by more than 50%, and the deadline satisfaction rate approaches 100%.

13:30-15:00

Technical Sessions for all conferences.

13:30-15:00 Session S7 - HSCC: Abstractions and Planning for Complex Control Systems
Location: Emerald Bay A
13:30
Memory-dependent abstractions of stochastic systems through the lens of transfer operators

ABSTRACT. With the increasing ubiquity of safety-critical autonomous systems operating in uncertain environments, there is a need for mathematical methods for formal verification of stochastic models. Towards formally verifying properties of stochastic systems, methods based on discrete, finite Markov approximations -- abstractions -- thereof have surged in recent years. These are found in contexts where: either a) one only has partial, discrete observations of the underlying continuous stochastic process, or b) the original system is too complex to analyze, so one partitions the continuous state-space of the original system to construct a handleable, finite-state model thereof. In both cases, the abstraction is an approximation of the discrete stochastic process that arises precisely from the discretization of the underlying continuous process. The fact that the abstraction is Markov and the discrete process is not (even though the original one is) leads to approximation errors. Towards accounting for non-Markovianity, we introduce memory-dependent abstractions for stochastic systems, capturing dynamics with memory effects. Our contribution is twofold. First, we provide a formalism for memory-dependent abstractions based on transfer operators. Second, we quantify the approximation error by upper bounding the total variation distance between the true continuous state distribution and its discrete approximation.

13:55
Scalable control synthesis for stochastic systems via structural IMDP abstractions

ABSTRACT. This paper introduces a novel abstraction-based framework for controller synthesis of nonlinear discrete-time stochastic systems. Thefocus is on probabilistic reach-avoid specifications. The framework is based on abstracting a stochastic system into a new class of ro-bust Markov models, called orthogonally decoupled Interval Markov Decision Processes (odIMDPs). Specifically, an odIMDPs is a classof robust Markov processes, where the transition probabilities between each pair of states are uncertain and have the product form.We show that such a specific form in the transition probabilities allows one to build compositional abstractions of stochastic systemsthat, for each state, are only required to store the marginal probability bounds of the original system. This leads to improved memorycomplexity for our approach compared to commonly employed abstraction-based approaches. Furthermore, we show that an optimal control strategy for a odIMDPs can be computed by solving a set of linear problems. When the resulting strategy is mapped back to the original system, it is guaranteed to lead to reduced conservatism compared to existing approaches. To test our theoretical framework, we perform an extensive empirical comparison of ourmethods against Interval Markov Decision Process- and Markov Decision Process-based approaches on various benchmarks including 7D systems. Our empirical analysis shows that our approach substantially outperforms state-of-the-art approaches in terms of both memory requirements and the conservatism of the results.

14:20
Multi-layer Motion Planning with Kinodynamic and Spatio-Temporal Constraints

ABSTRACT. We propose a novel, multi-layered planning approach for computingpaths that satisfy both kinodynamic and spatiotemporal constraints.Our three-layer framework first establishes potential sequences tomeet spatial constraints, using it to calculate a geometric lead path.This path then guides an asymptotically optimal sampling-basedkinodynamic planner, which minimizes an STL-robustness costto jointly satisfy spatiotemporal and kinodynamic constraints. Inour experiments, we test our method with a velocity-controlledAckerman-car model and demonstrate significant efficiency gainscompared to pure STL-cost encoding approaches. Additionally, ourmethod is also able to generate complex path maneuvers, such ascrossovers, something that previous methods had not demonstrated.

14:45
Robust Aggregation of Electric Vehicle Flexibility

ABSTRACT. We address the problem of characterizing the aggregate flexibility in populations of electric vehicles (EVs) with uncertain charging requirements.We extend upon prior results that provide exact characterizations of aggregate flexibility in electric vehicle (EV) populations by adapting the framework to encompass more general charging requirements. In doing so we give a characterization of the exact aggregate flexibility as a \textit{generalized polymatroid}. Furthermore, this paper advances these aggregation methodologies to address the case in which charging requirements are uncertain. In this extended framework, requirements are instead sampled from a specified distribution. In particular, we construct \textit{robust aggregate flexibility sets}, sets of aggregate charging profiles over which we can provide probabilistic guarantees that actual realized populations will be able to track. By leveraging measure concentration results that establish powerful finite sample guarantees, we are able to give tight bounds on these robust flexibility sets, even in low sample regimes that are well suited for aggregating small populations of EVs. We detail explicit methods of calculating these sets. Finally, we provide numerical results that validate our results and case studies that demonstrate the applicability of the theory developed herein.

13:30-15:00 Session S7 - ICCPS: Privacy, Trust, Honeypots
Chair:
Location: Emerald Bay B
13:30
PLCpot: Application Dialogue Replay based Scalable PLC Honeypot for Industrial Control Systems

ABSTRACT. Programmable Logic Controllers (PLCs) are essential components of industrial control systems (ICS), overseeing critical processes like manufacturing and power generation. As cyberattacks growin 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 byanalyzing 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 involvinga 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.

13:52
Atlas: Ensuring Accuracy for Privacy-Preserving Federated IoT Applications

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\%.

14:14
Trust-Based Assured Sensor Fusion in Distributed Aerial Autonomy

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.

14:36
Synthesis of Dynamic Masks for Information-Theoretic Opacity in Stochastic Systems

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.

13:30-15:00 Session S7 - RTAS: Security and Safety
Location: Emerald Bay CDE
13:30
A Design Flow to Securely Isolate FPGA Bus Transactions in Heterogeneous SoCs

ABSTRACT. Embedded computing systems are becoming increasingly complex. Modern system-on-chips come with heterogeneous designs that integrate diverse processing systems and a large variety of peripherals. When considering software with mixed and independent security and criticality levels, the heterogeneity of modern computing platforms poses considerable challenges in achieving strong isolation between execution domains. Tackling these challenges is even more difficult in platforms that integrate Field-Programmable Gate Array (FPGA) fabrics, which, due to their wide flexibility, introduce new security- and safety-related threats that can jeopardize isolation. As a matter of fact, if no proper countermeasures are in place, hardware accelerators (HAs) deployed on FPGA can be exploited to break the isolation capabilities implemented in a system by issuing dangerous bus transactions. This research proposes a design flow for heterogeneous platforms to strongly isolate bus transactions issued by HAs. The design flow is then specialized for the AMD Zynq UltraScale+ platform, leveraging the virtualization-related features of the Arm System Memory Management Unit (SMMU). The proposed solution jointly combines two new IPs for enforcing information transported by the AXI bus, a tool to verify the FPGA design, a principled configuration of the SMMU driver, and a secure boot flow. The proposal is evaluated with an industry-relevant use case related to embedded machine learning applied for the railway domain, in which isolation is established between two AMD Deep Learning Processor Units (DPU) and a set of FPGA HAs dedicated to a real-time critical application.

13:52
Janus: OS Support for a Secure, Fast Control-Plane

ABSTRACT. The emergence of the edge cloud, empowered by advanced wireless technologies such as 5G, is aimed at delivering predictable latency-sensitive services with the potential for interaction within low milliseconds. Even in the traditional cloud, latency-sensitive services are pervasive. To enable low-latency software, much focus has been on data-plane optimizations for fast processing of requests. Unfortunately, these efforts alone are insufficient: effective low-latency service also require advances in the control-plane. However, control-plane operations require strong spatial and temporal isolation between tenant computations, thus can result in significant overhead.

This paper introduces Janus an OS abstraction for a flexible control-plane which provides strong isolation as well as managed latency through the use of pervasive kernel-bypass. Janus leverages hardware Memory Protection Key (MPK) to enable low-cost control operations for protected procedure call (PPC) and thread dispatch – two essential building blocks of spatial and temporal isolation. By transparently improving these fundamental control-plane operations, Janus enables efficient and predictable user-defined and customizable system control policies and mechanisms, while maintaining strong isolation. We evaluate Janus’s ability to define new control operations, increase the efficiency of an existing RTOS, and support low-latency services in a memcached server. Compared to a Linux approach, a specialized latency-sensitive control plane using Janus provides over a 6x improvement in throughput, while providing 99th percentile tail latencies almost 3x lower. In a multi-tenant system, tail latency improves by orders of magnitude.

14:14
Integrated Real-Time Control and Scheduling for Safety Critical Cyber-Physical Systems

ABSTRACT. Cyber-physical systems (CPS) ranging from autonomous vehicles to medical devices to earthquake engineering experiments must interact with varying environments at fine-grained time-scales, assuring control safety and stability while optimizing application-specific performance objectives. To address those requirements, co-design of real-time control and scheduling has received considerable attention over multiple decades, to allow rigorous assurance of system properties while enabling diverse forms of adaptation to changing operating conditions.

In this paper, we present a new formalization of the periodicity requirements for control inputs to (1) guarantee reachability of safe (and avoidance of unsafe) portions of the system state space, (2) adaptively manage dynamic periodicity constraints that may change as the state space is traversed, and (3) express minimum periods to enable safe hand-offs between high-performance controllers and more conservative backup controllers. Our evaluations of this approach confirm that it is able to maintain system safety and stability while optimizing system performance.

14:36
Recovery-Guaranteed Sensor Attack Detection for Cyber-Physical Systems

ABSTRACT. Sensor attacks on Cyber-Physical Systems (CPS) can cause substantial damage in the physical world, which motivates two major threads of defense works including attack detection and attack recovery. The former aims to identify whether any sensors are compromised while the latter seeks to restore a system to safety once an attack is detected. Although either thread has drawn many efforts, how to coordinate the detection and recovery has been barely studied. Overlooking the coordination, existing works may result in ineffective and even failed defense. For example, if a detector raises an alarm too late, there may not be enough time for a system to recover but reach the unsafe region anyway, even though the detection result is accurate. By contrast, raising an alarm earlier allows more time for recovery, but may come with more false positives and thus unnecessarily trigger the recovery. To fill this gap, we aim to co-design attack detection and recovery, and propose a novel recovery-guaranteed sensor attack detection framework. The framework dynamically adjusts the detection sensitivity and authenticates state estimates at run time to guarantee timely and safe recovery once an attack is detected. The detection will always reserve sufficient time for the recovery while minimizing unnecessary activation of recovery. We conduct extensive simulations and real-world testbed experiments to show the efficiency of our solution.

13:30-15:00 Session S7 - SenSys: Advanced Wireless and Networked Sensing Systems
13:30
SARLink: Satellite Backscatter Connectivity using Synthetic Aperture Radar

ABSTRACT. SARLink is a passive satellite backscatter communication system that uses existing spaceborne synthetic aperture radar (SAR) imaging satellites to provide connectivity in remote regions. It achieves orders of magnitude more range than traditional backscatter systems, enabling communication between a passive ground node and a satellite in low earth orbit. The system is composed of a cooperative ground target, a SAR satellite, and a data processing algorithm. A mechanically modulating reflector was designed to apply amplitude modulation to ambient SAR backscatter signals by changing its radar cross section. These communication bits are extracted from the raw SAR data using an algorithm that leverages subaperture processing to detect multiple bits from a target in a single image dataset. A theoretical analysis of this communication system using on-off keying is presented, including the expected signal model, throughput, and bit error rate. The results suggest a 5.5 ft by 5.5 ft modulating corner reflector could send 60 bits every satellite pass, enough to support low bandwidth sensor data and messages. Using the SAR system Sentinel-1A, a satellite at an altitude of 693 km, we deployed static and modulating reflectors to evaluate the system. The results, successfully detecting the changing state of a modulating ground target, demonstrate our algorithm's effectiveness for extracting bits, paving the way for ultra-long-range, low-power satellite backscatter communication.

13:45
I4C... Improving I2C’s Dynamism and Efficiency

ABSTRACT. I2C is a popular interconnect bus for integrated circuits that employs an open-drain design to support multiple controllers. Originally designed for television motherboards with a static configuration of chips, I2C is now used in nearly every corner of electronics, from wearables to phones to satellites. Some emerging applications, however, are more dynamic and distributed than I2C can support today, limiting its utility. In particular, one typically static, design-time parameter—the value of a pull-up resistor—is chosen to roughly match the total distributed bus and gate capacitance, ensuring a pull-up rise time that satisfies the I2C spec. But with greater dynamism—when many I2C nodes are added or removed at run-time—a static pull-up resistor can lead to a bus that is at best inefficient and at worst inoperable. In this paper, we present a system that can measure the rise time in situ and at I2C data rates, allowing us to optimally adjust the pull-up resistor at run-time. With this rise time measurement capability in hand, we show how it can be used for other useful and novel functions, including detecting when I2C nodes are added or removed, enabling an efficient inband-interrupt signaling scheme that eliminates the need for interrupt polling, and even full-duplex reverse data transfer encoded into clock edges. We implement our design, called I4C, using commercial microcontrollers and discrete electronics, and evaluate it on a testbed of several nodes, demonstrating its viability and efficiency.

14:00
MoLoRa: Intelligent Mobile Antenna System for Enhanced LoRa Reception in Urban Environments

ABSTRACT. LoRa technology promises to enable Internet of Things applications over large geographical areas. However, its performance is often hampered by poor channel quality in urban environments, where blockage and multipath effects are prevalent. Our study uncovers that a slight shift in the position or attitude of the receiving antenna can substantially improve the received signal quality. This phenomenon can be attributed to the rich multipath characteristics of wireless signal propagation in urban environments, wherein even small antenna movement can alter the dominant signal path or reduce the polarization angular difference between transceivers. Leveraging these key observations, we propose and implement MoLoRa, an intelligent mobile antenna system designed to enhance LoRa packet reception. At its core, MoLoRa represents the position and attitude of an antenna as a state and employs a statistical optimization method to search for states that offer optimal signal quality efficiently. Through extensive evaluation, we demonstrate that MoLoRa achieves a maximum Signal-to-Noise Ratio (SNR) gain of 13 dB in a few attempts, enabling formerly problematic blind spots to reconnect and strengthening links for other nodes.

14:15
FlexiFly: Interfacing the Physical World with Foundation Models Empowered by Reconfigurable

ABSTRACT. Foundation models (FM) have shown immense human-like capabilities for generating digital media. However, foundation models that can freely sense, interact, and actuate the physical domain is far from being realized. This is due to 1) requiring dense deployments of sensors to fully cover and analyze large spaces, while 2) events often being localized to small areas, making it difficult for FMs to pinpoint relevant areas of interest relevant to the current task. We propose FlexiFly a platform that enables FMs to “zoom in” and analyze relevant areas with higher granularity to better understand the physical environment and carry out tasks. FlexiFly accomplishes by introducing 1) a novel image segmentation technique that aids in identifying relevant locations and 2) a modular and reconfigurable sensing and actuation drone platform that FMs can actuate to “zoom in” with relevant sensors and actuators. We demonstrate through real smart home deployments that FlexiFly enables FMs and LLMs to complete diverse tasks up to 85% more successfully. FlexiFly is critical step towards FMs and LLMs that can naturally interface with the physical world.

14:30
Offload Rethinking by Cloud Assistance for Efficient Environmental on LPWANs

ABSTRACT. Learning-based environmental sound recognition has emerged as a crucial method for ultra-low-power environmental monitoring in biological research and city-scale sensing systems. These systems usually operate under limited resources and are often powered by harvested energy in remote areas. Recent efforts in on-device sound recognition suffer from low accuracy due to resource constraints, whereas cloud offloading strategies are hindered by high communication costs. In this work, we introduce ORCA, a novel resource-efficient cloud-assisted environmental sound recognition system on batteryless devices operating over the Low-Power Wide-Area Networks (LPWANs), targeting wide-area audio sensing applications. We propose a cloud assistance strategy that remedies the low accuracy of on-device inference while minimizing the communication costs for cloud offloading. By leveraging a self-attention-based cloud sub-spectral feature selection method to facilitate efficient on-device inference, ORCA resolves three key challenges for resource-constrained cloud offloading over LPWANs: 1) high communication costs and low data rates, 2) dynamic wireless channel conditions, and 3) unreliable offloading. We implement ORCA on an energy-harvesting batteryless microcontroller and evaluate it in a real world urban sound testbed. Our results show that ORCA outperforms state-of-the-art methods by up to 80×80× in energy savings and 220×220× in latency reduction while maintaining comparable accuracy.

14:45
Mitigating In-Transit Vision Noise for Enhanced Vehicle Safety

ABSTRACT. Software-defined vehicles (SDVs) rely on cameras for intelligent and safety-critical applications but face challenges from dynamic environmental noise, including weather and occlusions. Unlike static sensors, SDV cameras encounter noise patterns influenced by driving speed, a factor often overlooked in prior research. To address this gap, we conduct a quantitative analysis of the in-transit noise impact using data from public datasets, the CARLA simulator, a robotic vehicle, and a real vehicle. Our findings suggest that maintaining a speed below 40km/h may serve as a threshold for ensuring reliable camera-based applications under noisy urban conditions. In addition, we propose TransitNet, a novel model designed to mitigate in-transit camera noise and enhance driving safety, particularly at higher speeds. Compared to multiple baselines, experimental results show that TransitNet improves the F-measure by 5.1%, mAP@50 by 3.6%, and increases FPS by 56.7% across all datasets. We also provide detailed observations and insights from extensive testing.

15:30-17:30

Technical Sessions for all conferences.

15:30-17:30 Session S8 - HSCC: Behavioral Verification and Synthesis for Hybrid and Learning Systems
Location: Emerald Bay A
15:30
Distributionally Robust Statistical Verification with Imprecise Neural Networks

ABSTRACT. A particularly challenging problem in AI safety is providing guarantees on the behavior of high-dimensional autonomous systems. Verification approaches centered around reachability analysis fail to scale, and purely statistical approaches are constrained by the distributional assumptions about the sampling process. Instead, we pose a distributionally robust version of the statistical verification problem for black-box systems, where our performance guarantees hold over a large family of distributions. This paper proposes a novel approach based on a combination of active learning, uncertainty quantification, and neural network verification. A central piece of our approach is an ensemble technique called Imprecise Neural Networks, which provides the uncertainty to guide active learning. The active learning uses an exhaustive neural-network verification tool Sherlock to collect samples. An evaluation on multiple physical simulators in the openAI gym Mujoco environments with reinforcement-learned controllers demonstrates that our approach can provide useful and scalable guarantees for high-dimensional systems.

15:54
ProbStar Temporal Logic for Verifying Complex Behaviors of Learning-enabled Systems

ABSTRACT. This paper introduces a novel quantitative verification framework for analyzing the temporal behaviors of learning-enabled systems (LES). Our approach employs ProbStar Temporal Logic (ProbStarTL) to specify LES temporal behaviors alongside advanced reachability and verification algorithms. Unlike existing qualitative methods focusing primarily on reach-avoid properties, our framework enables quantitative analysis of temporal properties. ProbStarTL, distinct from Signal Temporal Logic, operates on sequences of timed probabilistic star reachable sets, known as ProbStar signals. It features a clear syntax and dual qualitative and quantitative semantics. Our framework includes depth-first search algorithms for generating ProbStar traces and novel verification algorithms that transform ProbStarTL specifications into a computable disjunctive normal form for analysis. Our verification algorithms allow for both exact and approximate analyses. The exact scheme guarantees sound and complete results with precise satisfaction probabilities, while the approximate scheme offers sound results with maximum and minimum satisfaction probabilities at a reduced computational cost. The new verification framework is implemented using StarV, and its effectiveness is demonstrated through case studies on a learning-based adaptive cruise control system and an advanced emergency braking system.

16:18
BT2Automata: Expressing Behavior Trees as Automata for Formal Control Synthesis

ABSTRACT. This research presents a novel approach to bridging the gap between the interpretable and flexible nature of Behavior Trees (BTs) and the rigorous formal verification and synthesis capabilities of temporal logics. Temporal logics, such as Linear Temporal Logic (LTL) and Metric Interval Temporal Logic (MITL), are widely used for task specification due to their intuitive syntax for expressing temporally evolving behaviors. However, encoding complex task dependencies and recovery actions in temporal logic can lead to intractability. BTs, known for their modular structure and dynamic adaptability, have gained popularity in robotics for task specification. Despite the advantages of BTs, their flexible structure complicates formal analysis for safety and performance guarantees, limiting their use in control synthesis. This work presents a novel approach by translating BTs into Timed Automata (TA), thus enabling falsification (counterexample generation) with UPPAAL to identify inconsistencies and ensure language completeness, especially when defined with timing constraints. This integration allows for the detection of potential inconsistencies, the monitoring of temporal properties, and the synthesis of automaton and sampling based control strategies that guarantee satisfaction of task objectives.

16:42
Exploring Behaviors of Hybrid Systems via the Voronoi Bias over Output Signals

ABSTRACT. In this paper, we consider an analysis of temporal properties of hybrid systems based on simulations, so-called falsification of requirements. We present a novel exploration-based algorithm for falsification of black-box models of hybrid systems based on the Voronoi bias in the output space. This approach is inspired by techniques used originally in motion planning: rapidly exploring random trees. Instead of commonly employed exploration that is based on coverage of inputs, the proposed algorithm aims to cover all possible outputs directly. Compared to other state-of-the-art falsification tools, it also does not require robustness or other guidance metrics tied to a specific behavior that is being falsified. This allows our algorithm to falsify specifications for which robustness is not conclusive enough to guide the falsification procedure.

17:06
Explaining Control Policies through Predicate Decision Diagrams

ABSTRACT. Safety-critical controllers of complex systems are hard to construct manually. Automated approaches such as controller synthesis or learning provide a tempting alternative but usually lack explainability. To this end, learning decision trees (DTs) has been prevalently used towards an interpretable model of the generated controllers. However, DTs do not exploit shared decision making, a key concept exploited in binary decision diagrams (BDDs) to reduce their size and thus improve explainability. In this work, we introduce predicate decision diagrams (PDDs) that extend BDDs with predicates and thus unite the advantages of DTs and BDDs for controller representation. We establish a synthesis pipeline for efficient construction of PDDs from DTs representing controllers, exploiting reduction techniques for BDDs also for PDDs.

15:30-16:41 Session S8 - ICCPS: Robotic and Autonomous Systems
Location: Emerald Bay B
15:30
Optimal Integrated Task and Path Planning for Collaborative Multi-Robot Systems

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.

15:52
RLS3: RL-Based Synthetic Sample Selection to Enhance Spatial Reasoning in Vision-Language Models for Indoor Autonomous Perception

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.

16:14
Accelerating Neural Policy Repair with Preservation via Stability-Plasticity Interpolation

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.

16:36
Closing Remarks

ABSTRACT. Closing remarks from the Program co-Chairs.

15:30-17:30 Session S8 - RTAS: Cloud and Edge Computing
Location: Emerald Bay CDE
15:30
Scheduling Job Streams on Uniprocessors with Cold Start Delays

ABSTRACT. We consider uniprocessor job scheduling where jobs have deadlines and each job belongs to a job family. Each job family has an associated setup time or cold start delay, and when a job is scheduled, if the predecessor job does not belong to the same job family then this setup time needs to be included. We examine the scheduling problem when the objective is to minimize the number of tardy jobs, and the challenge of including the setup time for switching between job families results in poor performance of well-known policies such as earliest deadline first (EDF). We propose a near-optimal online scheduling policy for jobs with deadlines, on uniprocessor platforms. This problem arises in a variety of contexts including serverless computing and MLaaS (machine learning as a service) where a job request may need a suitable resource container to be provisioned if an earlier request was not of the same type. The general offline problem of job scheduling with job families and setup costs has previously been studied and shown to be NP-Hard. In an effort to improve our understanding of the online problem with the objective of maximizing the number of jobs that meet their deadlines, we focus on the case where all jobs have the same execution time. We show that even this special case is NP-Hard in the offline setting. The policy we propose, which requires job buffering, is nearly 1-competitive when each job has a reasonably large slack. We also propose a heuristic that performs well in many situations despite a weak competitive ratio.

15:52
MATCH: Real-Time Scheduling of Multiple and Parallel Data Copies in Heterogeneous Architectures

ABSTRACT. In recent years, multiple data copies become popular in heterogeneous computing architectures. They enable parallel data transfer among diverse processing units. Tasks executed on such heterogeneous architectures often exhibit heightened resource competitions and intricate task dependencies, posing challenges in meeting strict timing constraints. Due to the dominant roles of data copies in the heterogeneous architecture, effective scheduling and tight response time analysis could contribute to the timing performance of the entire heterogeneous computing system. In this work, we introduce MATCH, which offers real-time scheduling and end-to-end response time analysis for the multiple parallel data copies that are popular in mainstream heterogeneous architectures. We first identify the aggravated resource competition and task dependency from multiple data copies and comprehensive task execution patterns. Then, we provide a real-time scheduling strategy and cross-granularity schedulability analysis to deal with resource competition and task dependency. Extensive evaluation demonstrates that efficient scheduling and analysis on multiple parallel data copies can significantly improve the schedulability by 55.5%-144.4%. Additionally, experiments conducted on various scales of heterogeneous systems demonstrate that MATCH can significantly reduce pessimism in response time analysis by up to 22.8%-57.5%. Importantly, the proposed approach is compatible with existing scheduling approaches that do not consider multiple parallel data copies and are readily applied to off-the-shelf heterogeneous computing systems.

16:14
Scheduling Processing Graphs of Gang Tasks on Heterogeneous Platforms

ABSTRACT. Real-time systems with artificial-intelligence-powered autonomous functionalities typically consist of numerous gang tasks, such as computations on graphics processing units (GPUs), that are interconnected by data-flow dependencies. Despite their relevance in many applications, scheduling processing graphs of gang tasks has received limited attention. This paper presents scheduling techniques and response-time analysis for such systems on heterogeneous computing platforms. Response-time bounds of a graph of gang tasks are presented when scheduled under a work-conserving or semi-work-conserving scheduler. Techniques to support multiple graphs using federated scheduling techniques are also presented. Experimental evaluations and a case study on a computer vision application are presented to demonstrate the effectiveness of the proposed approach.

16:36
A Framework for Managing Edge-Cloud Distributed Embedded Systems

ABSTRACT. We introduce ANON, a novel framework for lightweight virtualization and orchestration of distributed real-time systems. Leveraging WebAssembly (Wasm) for robust sandboxing and multi-language (polyglot) capabilities, ANON decouples applications from their platforms through distinct manifests, enabling a centralized orchestrator to optimize resource allocation and deploy Wasm modules seamlessly across the edge-cloud continuum. It features a split data and control plane with orchestration sidecars, allowing applications to use native communication protocols and respond autonomously to network changes. We evaluate our framework in two real application contexts: an industrial automation use-case and an automotive body electronics demonstrator. Through micro-benchmarks and end-to-end testing, we demonstrate ANON’s potential for managing real-time workloads in diverse heterogeneous ecosystems.

16:58
HARD: Hardening Real-Time Scheduling and Analysis for Accelerator Enabled Computing

ABSTRACT. Despite continuous advancements in artificial intelligence, accelerator-enabled computing architecture faces challenges in meeting strict timing constraints due to the complex interactions between CPU cores and accelerators. Although various scheduling and response time analysis techniques have been developed, a considerable gap due to pessimism remains between hard real-time performance (i.e., derived worst-case response time) and soft real-time performance (i.e., actual response time in runtime measurement on real systems). To address this issue, we propose HARD, a real-time scheduling approach that integrates scheduling strategies, response time analysis, and practical scheduler designs for general accelerator-enabled computing platforms. HARD effectively improves theoretically guaranteed hard real-time performance given the similar runtime measurement-based soft real-time performance. Comprehensive experiments on off-the-shelf Intel CPU and NVIDIA GPU systems demonstrate that HARD outperforms state-of-the-art scheduling and analysis approaches, achieving a 27.3% improvement in hard real-time performance, a 3.7% improvement in soft real-time performance, and a remarkable 45.1% reduction in pessimism. The proposed HARD approach shows great potential in improving the runtime timing performance of accelerator-enabled architectures.

17:20
Closing Remarks
15:30-17:30 Session S8 - SenSys: Multi-modal Human & Environmental Sensing
Chair:
15:30
MMBind: Unleashing the Potential of Distributed and Heterogeneous Data for Multimodal Learning in IoT

ABSTRACT. Multimodal sensing systems are increasingly prevalent in various real-world applications. Most existing multimodal learning approaches heavily rely on training with a large amount of synchronized, complete multimodal data. However, such a setting is impractical in real-world IoT sensing applications where data is typically collected by distributed nodes with heterogeneous data modalities, and is also rarely labeled. In this paper, we propose MMBind, a new data binding approach for multimodal learning on distributed and heterogeneous IoT data. The key idea of MMBind is to construct a pseudo-paired multimodal dataset for model training by binding data from disparate sources and incomplete modalities through a sufficiently descriptive shared modality. We also propose a weighted contrastive learning approach to handle domain shifts among disparate data, coupled with an adaptive multimodal learning architecture capable of training models with heterogeneous modality combinations. Evaluations on ten real-world multimodal datasets highlight that MMBind outperforms state-of-the-art baselines under varying degrees of data incompleteness and domain shift, and holds promise for advancing multimodal foundation model training in IoT applications.

15:45
BioQ: Towards Context-Aware Multi-Device Collaboration with Bio-cues

ABSTRACT. The rapid growth of wearable devices has opened exciting opportunities for context-aware multi-device collaboration, where multiple devices can provide enhanced user experience tailored to user needs and conditions. However, it also presents a unique challenge of reliably determining whether a set of wearables is being used by the same individual. In real-world scenarios, device sharing, exchanging, or unintended use can cause privacy risks and degraded functionality. Existing solutions primarily rely on accelerometer data to match movement patterns across devices, but they perform poorly during stationary or varied non-repetitive activities. In this paper, we introduce BioQ, a method that unobtrusively detects wearable co-location by generating and matching bio-cues. These bio-cues are generated from on-body wearable sensor data and embedded into a common latent space. Furthermore, when devices share the same sensor types, BioQ can effectively integrate multiple sensor sources to improve cue generation and matching. Experimental results show that BioQ outperforms baselines in bio-cue generation and matching and is resource-effective in model training, inference, and energy use. Our code is available at https://github.com/Nokia-Bell-Labs/contextual-biological-cues.

16:00
PIPE: Privacy-preserving 6DoF Pose Estimation for Immersive Applications

ABSTRACT. Image-based mapping and localization offer six degrees of freedom (6DoF) pose estimation for immersive applications. This is achieved by matching, on a server, 2D visual features extracted from a mobile device’s camera view and 3D features stored in a map. While effective, this process may lead to privacy breaches (e.g., exposure of sensitive information captured by camera views). To tackle this crucial issue, we present PIPE, a first-of-its-kind Privacy-preserving Image-based 6DoF Pose Estimation system. The design of PIPE is motivated by our key observation that uploading only a small amount of features extracted from camera views for pose estimation could reduce privacy leakage. However, trade-offs exist between privacy preservation, system utility (i.e., pose estimation accuracy), and system performance (e.g., end-to-end latency). To balance the trade-offs, PIPE deliberately explores the feature-detection space to reduce computation latency, designs an efficient feature ranking method by judiciously utilizing map data, and optimizes feature selection by jointly considering the features’ ranking and spatial distribution to improve pose estimation accuracy. Moreover, we construct a learning-based metric to quantify the extent of privacy leakage in images. Our extensive performance evaluation reveals that PIPE can effectively preserve privacy and reduce end-to-end latency by up to 22.6%, while marginally affecting pose estimation accuracy (e.g., as low as 2.7%).

16:15
ThermoHands: A Benchmark for 3D Hand Pose Estimation from Egocentric Thermal Images

ABSTRACT. Designing egocentric 3D hand pose estimation systems that can perform reliably in complex, real-world scenarios is crucial for downstream applications. Previous approaches using RGB or NIR imagery struggle in challenging conditions: RGB methods are susceptible to lighting variations and obstructions like handwear, while NIR techniques can be disrupted by sunlight or interference from other NIR-equipped devices. To address these limitations, we present ThermoHands, the first benchmark focused on thermal image-based egocentric 3D hand pose estimation, demonstrating the potential of thermal imaging to achieve robust performance under these conditions. The benchmark includes a multi-view and multi-spectral dataset collected from 28 subjects performing hand-object and hand-virtual interactions under diverse scenarios, accurately annotated with 3D hand poses through an automated process. We introduce a new baseline method, TherFormer, utilizing dual transformer modules for effective egocentric 3D hand pose estimation in thermal imagery. Our experimental results highlight TherFormer's leading performance and affirm thermal imaging's effectiveness in enabling robust 3D hand pose estimation in adverse conditions.

16:30
Geoduck: Nanosatellite Constellation Scheduling for Low Latency Event Detection

ABSTRACT. Commercial companies have launched hundreds of small, low-cost nanosatellites for Earth observation tasks, such as monitoring forest fires, landslides, and lake algae. These time-critical events require low-latency detection. Previous work has shown that capture latency, defined as the duration between an event occurrence and a satellite capturing an image covering the event region, is the major latency component. In this work, we ask what the minimum capture latency is under physical orbital dynamics and energy constraints. We first characterize how region location and satellite orbital configuration affect the capture latency. Next, we explore the scheduling of satellite captures when energy constraints prevent the capture of all images. We introduce Geoduck, a satellite capture scheduler specifically designed to minimize capture latency. Geoduck leverages the insight that the timing of many events follows a prior distribution; for example, forest fires are more likely to occur in summer. We analyze the impact of different capture schedules on latency and propose a dynamic programming algorithm to choose the optimal captures. Our evaluation shows that Geoduck reduces capture latency by 1.5–2.1×.

16:45
CaphandAuth: Robust and Anti-spoofing Hand Authentication via COTS Capacitive Touchscreens

ABSTRACT. Utilizing unique physiological or behavioral traits, biometrics offers an intuitive authentication approach. However, common biometric modalities are susceptible to ambient factors and privacy concerns. This paper proposes CaphandAuth, a novel capacitive touchscreen-based hand authentication system. Using intrinsic capacitive imaging within the touchscreen, it provides a new secure, cost-effective, and user-friendly biometric authentication solution that is inherently resilient to environmental factors. To this end, CaphandAuth captures consecutive capacitive frames as the hand moves across the touchscreen. These frames are processed with an innovative super-resolution algorithm tailored for deformable objects to enhance details. A learning-based feature extractor then derives expressive and adaptive feature representations from the enhanced images. Extensive experiments demonstrate that CaphandAuth achieves an authentication accuracy of 99.84% and an equal error rate (EER) of 2.77% on a commercial tablet. Moreover, CaphandAuth exhibits formidable resilience to diverse deceiving attempts, including handprint simulation attacks, counterfeit spoofing attacks, and puppet attacks, making it a robust and secure solution in real-world scenarios.

17:00
Matching Skeleton-based Activity Representations with Heterogeneous Signals for HAR

ABSTRACT. In human activity recognition (HAR), activity labels have typically been encoded in one-hot format, which has a recent shift towards using textual representations to provide contextual knowledge. Here, we argue that HAR should be anchored to physical motion data, as motion forms the basis of activity and applies effectively across sensing systems, whereas text is inherently limited. We propose SKELAR, a novel HAR framework that pretrains activity representations from skeleton data and matches them with heterogeneous HAR signals. Our method addresses two major challenges: (1) capturing core motion knowledge without context-specific details. We achieve this through a self-supervised coarse angle reconstruction task that recovers joint rotation angles, invariant to both users and deployments; (2) adapting the representations to downstream tasks with varying modalities and focuses. To address this, we introduce a self-attention matching module that dynamically prioritizes relevant body parts in a data-driven manner. Given the lack of corresponding labels in existing skeleton data, we establish MASD, a new HAR dataset with IMU, WiFi, and skeleton, collected from 20 subjects performing 27 activities. This is the first broadly applicable HAR dataset with time-synchronized data across three modalities. Experiments show that SKELAR achieves the state-of-the-art performance in both full-shot and few-shot settings. We also demonstrate that SKELAR can effectively leverage synthetic skeleton data to extend its use in scenarios without skeleton collections.

17:15
RetroLiDAR: A Liquid-crystal Fiducial Marker System for High-fidelity Perception of Embodied AI

ABSTRACT. As embodied AI gradually transitions into practical applications, enhancing the fidelity of how embodied agents perceive the physical world has become a critical challenge. Current perception methods typically rely on computer vision-based fiducial marker systems, which suffer from limitations such as insufficient reading distance, poor localization accuracy, and high susceptibility to environmental lighting conditions. Currently, SPAD sensor-based LiDAR technology is emerging in commercial mobile devices due to its compact size, high precision, and low power consumption. This paper presents the design of the RetroLiDAR system, which chimes with the concept of backscatter in wireless technology, to create a liquid-crystal fiducial marker system that can be directly read by LiDAR. On the marker side, we use retroreflective materials to reflect the LiDAR's emitted light back and employ a liquid crystal modulator to adjust the intensity of the light signal. On the LiDAR end, we design a signal processing pipeline to demodulate the marker's modulation message using the temporal received signal strength. Experimental results from our prototype demonstrate that compared to visual fiducial markers, RetroLiDAR extends the reading distance by 2.6x compared to QR codes and by 44% compared to AprilTags, while reducing the median ranging error by 85%. We also present a low-power marker circuit design, a link budget analysis, and two proof-of-concept applications to validate the system's efficacy and practicality.