Framed around the motion “This House contends that the inherent complexity of modern engineering challenges renders exhaustive mathematical analysis overkill, and that an iterative, adaptive design approach should be prioritized—even for life-critical systems,” this session will feature structured arguments, audience participation, and live voting. With opening statements, cross-examination, and closing remarks from both teams, the debate aims to challenge assumptions, spark meaningful discussion, and engage the CPS-IoT Week community in one of the most pressing questions today.
Data-Driven Dynamic Controller Synthesis for Discrete-Time General Nonlinear Systems
ABSTRACT. Synthesizing safety controllers for general nonlinear systems is a highly challenging task, particularly when the system models are unknown, and input constraints are present. While some recent efforts have explored data-driven safety controller design for nonlinear systems, these approaches are primarily limited to specific classes of nonlinear dynamics (e.g., polynomials) and are not applicable to general nonlinear systems. This paper develops a direct data-driven approach for discrete-time general nonlinear systems, facilitating the simultaneous learning of control barrier certificates (CBCs) and dynamic controllers to ensure safety properties under input constraints. Specifically, by leveraging the adding-one-integrator approach, we incorporate the controller’s dynamics into the system dynamics to synthesize a virtual static-feedback controller for the augmented system, resulting in a dynamic safety controller for the actual dynamics. We collect input-state data from the augmented system during a finite-time experiment, referred to as a single trajectory. Using this data, we learn augmented CBCs and the corresponding virtual safety controllers, ensuring the safety of the actual system and adherence to input constraints over a finite time horizon. We demonstrate that our proposed conditions boil down to some data-dependent linear matrix inequalities (LMIs), which are easy to satisfy. We demonstrate the effectiveness of our data-driven approach through a case study involving highly nonlinear terms with unknown dynamics.
From Data to Global Asymptotic Stability of Unknown Large-Scale Networks with Provable Guarantees
ABSTRACT. We offer a compositional data-driven scheme for synthesizing controllers that ensure global asymptotic stability (GAS) across large-scale interconnected networks, characterized by unknown mathematical models. In light of each network's configuration composed of numerous subsystems with smaller dimensions, our proposed framework gathers data from each subsystem's trajectory, enabling the design of local controllers that ensure input-to-state stability (ISS) properties over subsystems, signified by ISS Lyapunov functions. To accomplish this, we require only a single input-state trajectory from each unknown subsystem up to a specified time horizon, fulfilling certain rank conditions. Subsequently, under small-gain compositional reasoning, we leverage ISS Lyapunov functions derived from data to offer a control Lyapunov function (CLF) for the interconnected network, ensuring GAS certificate over the network. We demonstrate that while the computational complexity for designing a CLF increases polynomially with the network dimension using sum-of-squares (SOS) optimization, our compositional data-driven approach significantly mitigates it to linear with respect to the number of subsystems. We showcase the efficacy of our data-driven approach over a set of benchmarks, involving physical networks with diverse interconnection topologies.
Robust Identification of Hybrid Automata from Noisy Data
ABSTRACT. In recent years, many different methods for identifying hybrid automata from data have been proposed. However, most of these methods consider clean simulator data, and consequently do not perform well for noisy data measured from real systems. We address this shortcoming with a new approach for the identification of hybrid automata that is specifically designed to be robust to noise. In particular, we propose a new high-level strategy consisting of the following three steps: clustering based on the dynamics identified from a local dataset, state space partitioning using decision trees, and conversion of the decision tree to a hybrid automaton. In addition, we introduce several new concepts for the realization of the single steps. For example, we propose an automated regularization of the dynamic models used for clustering via rank adaption, as well as a new variant of the Gini impurity index for decision tree learning, tailored toward hybrid systems where different dynamics can be active within the same state space region. As our experiments on 19 challenging benchmarks with different characteristics demonstrate, in addition to being robust to both process and measurement noise, our approach avoids the need for extensive hyper-parameter tuning and also performs well for clean data without noise.
SAVER: A Toolbox for Sampling-Based, Probabilistic Verification of Neural Networks
ABSTRACT. We present a neural network verification toolbox to 1) assess the probability of satisfaction of a constraint, and 2) synthesize a set expansion factor to achieve the probability of satisfaction. Specifically, the tool box establishes with a user-specified level of confidence whether the output of the neural network for a given input distribution is likely to be contained within a given set. Should the tool determine that the given set cannot satisfy the likelihood constraint, the tool also implements an approach outlined in this paper to alter the constraint set to ensure that the user-defined satisfaction probability is achieved. The toolbox is comprised of sampling-based approaches which exploit the properties of signed distance function to define set containment.
T-Tex: Timed Threaded Execution in Real-Time OpenMP
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
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
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
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.
A Unified Framework for Quantitative Cache Analysis (Outstanding Paper Award)
ABSTRACT. In this work we unify two existing lines of work towards cache analysis for non-LRU policies. To this end, we extend the notion of competitiveness to block-wise competitiveness and systematically analyze the competitiveness and block competitiveness of FIFO and MRU relative to LRU for arbitrary associativities. We show how competitiveness and block competitiveness can be exploited in state-of-the-art WCET analysis based on the results of existing persistence analyses for LRU. Unlike prior work, our approach is applicable to microarchitectures that exhibit timing anomalies. We experimentally evaluate the precision and cost of our approach on benchmarks from TACLeBench. The experiments demonstrate that quantitative cache analysis for FIFO and MRU comes close to the precision of LRU.
Consistency-aware and Predictable Memory Processing for Safety-critical Out-of-order Multicores
ABSTRACT. We investigate the memory hierarchy support for out-of-order multicore in safety-critical embedded systems (SCES) that enables memory level parallelism (MLP). Our work focuses on the timing predictability of memory accesses where memory accesses have guaranteed worst-case latency (WCL). Exploiting MLP requires an appropriate memory consistency model enforcement mechanism to ensure compliance with the instruction set architecture. General-purpose out-of-order cores retry memory requests when MCM violations occur, resulting in increased WCL. Predictable Processing of multiPle outstanding requests (PPP) is proposed as a mechanism to leverage the performance benefits while guaranteeing WCL through micro-architectural enhancements. Experimental evaluation demonstrates that PPP achieves speedups of 2.07×, 2.79×, and 3.38× compared to serialization, while maintaining analytically bounded WCL.
ParRP: Enabling Space Isolation in Caches with Shared Data
ABSTRACT. This work presents an approach to isolate cache space while supporting shared data. Enabling shared data caching is challenging because it causes interference making it unsuitable for real-time multicores. Unlike prior works, we aim to introduce isolation, but our approach enables caching of shared data, and promotes isolated cache analysis for individual cores. The crux behind our approach is that shared data isolation can be achieved by partitioning the replacement information instead of the cache's data storage. Consequently, this work introduces ParRP, a novel hardware cache partitioning scheme for real-time cache-coherent multicores. Our evaluation using the gem5 simulator shows that, by providing isolation for shared data, the worst-case execution time of multi-threaded tasks can be lower by 2.4x at the cost of a 16.5% decrease in average-case performance.
A Field Practical Approach to Memory Bandwidth Allocation for Consolidating Multi-Domain Automotive Applications on a Single SoC
ABSTRACT. Along with the advent of a high-end SoC with multiple CPU clusters and many GPUs, the automotive industry has a strong motivation to consolidate multi-domain applications on such a single SoC for wiring harness reduction and space/weight saving. For this, it is essential to bound their mutual interferences among CPU+GPU clusters on the system memory since advanced automotive applications use huge size code/data like autonomous driving and multi-screen infotainment. In order to guarantee memory bandwidth to each cluster, this paper proposes a cluster-level memory access regulation that aggregates the total memory access amount by each cluster (by all CPU cores and GPUs within the cluster) and throttles the cluster if it exceeds the given threshold. Then, we proposes a few-shot measurement based optimal memory bandwidth allocation that can find a near optimal solution with only a few measurements, which is practically essential to save the system development cost. Our extensive experiments on a real SoC board say that our proposed techniques successfully regulate each cluster's memory bandwidth usage within ±10% margin of the allocated bandwidth. Also, our optimization can achieve a near-optimal utility with less than 5% loss on average compared to the real optimal, with only a few measurements (mostly three or four measurements) instead of 61 measurements needed for the real optimal.
UMusic: In-car Occupancy Sensing via High-resolution UWB Power Delay Profile
ABSTRACT. Occupancy sensing is essential for vehicle safety and security applications such as seat belt reminders, airbag deployment, intrusion detection, and child-left-behind alerts. This paper presents UMusic, a novel in-car occupancy sensing system that reuses the ultra-wideband (UWB) devices already installed for access control in modern vehicles. However, due to the compact size and metal structure, the in-car environment is full of reflected propagation paths, which cannot be precisely resolved even with UWB's wide-bandwidth feature. To overcome this challenge, UMusic introduces a reflected-path decomposition technique to extract a high-resolution power delay profile (PDP) from the channel impulse response (CIR) provided by commodity UWB devices, enabling precise environmental perception. By comparing PDPs in empty and occupied conditions, UMusic is able to detect the occupancy status in both a sedan and an SUV with multiple passengers across various scenarios. Our results show that UMusic achieves a 90.2% detection rate using a single CIR measurement collected within 50 ms, outperforming the state-of-the-art by 15.7%. When aggregating six consecutive CIR measurements, UMusic reaches 99.4% accuracy, demonstrating its effectiveness for real-world deployment.
RAM-Hand: Robust Acoustic Multi-Hand Pose Reconstruction Using a Microphone Array
ABSTRACT. Using 3D hand poses as the input of user interfaces can enable many novel human-computer interaction applications. However, conventional solutions for precisely reconstructing the hand poses are either vision-based, which are compute-intensive and may cause privacy issues, or wearable devices-based, which are intrusive to users. In this paper, we propose RAM-Hand, a Robust Acoustic 3D Multi-Hand pose reconstruction system built on a microphone array. Our RAM-Hand system can support multiple hands and is designed for high adaptability to new scenarios with limited training data. Specifically, it should robustly accommodate variations in environment, subject, and hand positions. To achieve this, on one hand, we propose a customized signal processing pipeline to segment multiple hands' reflections and extract the features corresponding to each hand, then feed those features into a transformer-based neural network for precise pose reconstruction. On the other hand, to tackle the challenge that the training data is limited, we propose a series of data augmentation methods to generate virtual training data, and utilize contrastive learning to ensure our model behaves well on new subjects. We conduct extensive experiments on a real-world microphone array testbed to evaluate the performance of the proposed system. The results show that our RAM-Hand system can localize each hand joint with an average error of 10.71 mm, handle multiple hands, and generalize well to the above mentioned new scenarios.
LeekyFeeder: In-Air Gesture Control Through Leaky Acoustic Waves
ABSTRACT. We present LeekyFeeder, a mobile application that explores the acoustic signals leaked from headphones to reconstruct gesture motions around the ear for fine-grained gesture control.To achieve this goal, LeekyFeeder repurposes the speaker and a single feed-forward microphone on active noise cancellation (ANC) headphones as a SONAR system, using inaudible frequency-modulated continuous-wave (FMCW) signals to track gesture reflections for accurate sensing. Since this single-receiver SONAR system is unable to differentiate reflection angles and further disentangle signal reflections from different gesture parts, we draw on principles of multi-modal learning to frame gesture motion reconstruction as a multi-modal translation task and propose a deep learning-based approach to fill the information gap between low-dimensional FMCW ranging readings and high-dimensional 3D hand movements. We implement LeekyFeeder on a pair of Google Pixel Buds and conduct experiments to examine the efficacy and robustness of LeekyFeeder in various conditions. Experiments based on six gesture types inspired by Apple Vision Pro demonstrate that LeekyFeeder achieves a PCK performance of 89% at 3cm across ten users, with an average MPJPE and MPJRPE error of 2.71cm and 1.88cm, respectively.
LightLLM: A Versatile Large Language Model for Predictive Light Sensing
ABSTRACT. We propose LightLLM, a model that fine tunes pre-trained large language models (LLMs) for light-based sensing tasks. It integrates a sensor data encoder to extract key features, a contextual prompt to provide environmental information, and a fusion layer to combine these inputs into a unified representation. This combined input is then processed by the pre-trained LLM, which remains frozen while being fine-tuned through the addition of lightweight, trainable components, allowing the model to adapt to new tasks without altering its original parameters. This approach enables flexible adaptation of LLM to specialized light sensing tasks with minimal computational overhead and retraining effort. We have implemented LightLLM for three light sensing tasks: light-based localization, outdoor solar forecasting, and indoor solar estimation. Using real-world experimental datasets, we demonstrate that LightLLM significantly outperforms state-of-the-art methods, achieving 4.4x improvement in localization accuracy and 3.4x improvement in indoor solar estimation when tested in previously unseen environments. We further demonstrate that LightLLM outperforms ChatGPT-4 with direct prompting, highlighting the advantages of LightLLM's specialized architecture for sensor data fusion with textual prompts.
RoboTera: Non-Contact Friction Sensing for Robotic Grasping via Wireless Sub-Terahertz Perception
ABSTRACT. Sensing friction coefficient is vital for various cyber-physical system applications, including robotic grasping. We present RoboTera, a novel system for the non-contact coefficient of friction (COF) estimation using sub-Terahertz (sub-THz) perception in robotics for the first time. While advanced tactile sensors can provide friction inputs, they require direct contact, which might not be suitable for various applications. Non-contact estimation of friction between the gripper and a target object requires extracting the minute surface perturbations which is unfortunately not supported by existing imaging modalities (such as camera and LiDAR). Our key insight is that sub-THz signals are best suited to infer such information as their sub-millimeter wavelength is comparable with surface perturbations. Hence, impinging sub-THz waves on everyday objects creates diffuse backscattering whose spectral profile hints at surface texture properties. Leveraging this, we use sub-THz wireless signals to extract surface roughness. By integrating sub-THz-estimated roughness inputs with conventional image-based material classification schemes, RoboTera provides a non-contact and precise COF inference framework. Further, we exploit COF inferences to identify stable grasp configurations and improve grasping performance. Our experiments demonstrate an average accuracy of over 92% in COF estimation. We implemented RoboTera on a robotic arm to assess its real-world grasping performance, achieving a 31.8% average improvement across objects with diverse COF profiles and shapes.
LiDARMarker: Machine-friendly Road Markers for Smart Driving Systems
ABSTRACT. As assisted and autonomous driving systems become more prevalent, the need for accurate interpretation of road traffic signs is critical for driving safety and functionality. Current camera-based recognition methods face challenges due to the variability of traffic signs and environmental conditions, leading to potential inaccuracies. To address this, we propose LiDARMarker, a type of machine-readable traffic sign using infrared materials, making it invisible to human drivers but detectable by LiDAR-equipped vehicles. This paper introduces the design, fabrication, and efficient decoding methods of LiDARMarker. LiDARMarker is tailored to the emerging capabilities and needs of modern vehicles, enhancing their ability and accuracy in traffic sign recognition while avoiding interference with human drivers. Through the proposal of LiDARMarker, we aim to inspire the rethinking of the design of traffic sign systems in the context of modern vehicles.
N2Women (Networking Networking Women) is a discipline-specific community of researchers in the fields of networking and communications. N2Women encourages diversity and aims at fostering connections among under-represented women in this computing (https://n2women.comsoc.org/).
Monitoring Spatially Distributed Cyber-Physical Systems with Alternating Finite Automata
ABSTRACT. Modern cyber-physical systems (CPS) can consist of various networked components and agents interacting and communicating with each other. In the context of spatially distributed CPS, these connections can be dynamically dependent on the spatial configuration of the various components and agents. In these settings, robust monitoring of the distributed components is vital to ensuring complex behaviors are achieved, and safety properties are maintained. To this end, we look at defining the automaton semantics for the Spatio-Temporal Reach and Escape Logic (STREL), a formal logic designed to express and monitor spatio-temporal requirements over mobile, spatially distributed CPS. Specifically, STREL reasons about spatio-temporal behavior over dynamic weighted graphs. While STREL is endowed with well defined qualitative and quantitative semantics, in this paper, we propose a novel construction of (weighted) alternating finite automata from STREL specifications that efficiently encodes these semantics. Moreover, we demonstrate how this automaton semantics can be used to perform both, offline and online monitoring for STREL specifications using a simulated drone swarm environment.
Runtime Enforcement of CPS against Signal Temporal Logic
ABSTRACT. Cyber-Physical Systems (CPSs), especially those involving autonomy, need guarantees of their safety. Runtime Enforcement (RE) is a lightweight method to formally ensure that some specified properties are satisfied over the executions of the system. Hence, there is recent interest in the RE of CPS. However, existing methods are not designed to tackle specifications suitable for the hybrid dynamics of CPS. With this in mind, we develop runtime enforcement of CPS using properties defined in Signal Temporal Logic (STL).In this work, we aim to construct a runtime enforcer for a given STL formula to minimally modify a signal to satisfy the formula. To achieve this, the STL formula to be enforced is first translated into a timed transducer, while the signal to be corrected is encoded as timed words. We provide timed transducers for the temporal operators \emph{until} and \emph{release} noting that other temporal operators can be expressed using these two. Our approach enables effective enforcement of STL properties for CPS. A case study is provided to illustrate the approach and generate empirical evidence of its suitability for CPS.
Soteria: A Formal Digital-Twin-Enabled Framework for Safety-Assurance of Latency-Aware Safety-Critical Cyber-Physical Systems
ABSTRACT. Autonomous systems are integral to many safety-critical applications, such as industrial automation, autonomous vehicles, and the Industrial Internet of Things (IIoT). The verification of both functional and temporal correctness of these systems is crucial prior to deployment to ensure safety. However, due to the interaction of continuous-time dynamics in physical systems and discrete-time constraints in computational models, achieving end-to-end verification poses significant challenges. A promising solution is the development of a comprehensive "digital twin"---a model-based twin that mirrors the real system’s physical and computational behaviors. By creating this digital twin, we can rigorously assess and verify the system’s correctness within a virtual framework, capturing both physical dynamics and computational requirements. Most existing works in the real-time systems community are focused only on formal proofs of the temporal correctness of computational models, whereas the control system community addresses the continuous dynamics of physical processes and how to control them within `provided' real-time constraints. Unlike those, this digital twin approach allows for an integrated verification process that addresses both physical models and timing requirements, as well as their deep correlation concurrently. This paper introduces SOTERIA\footnote{SOTERIA was the Greek goddess of safety, deliverance, and preservation from harm.}, a hybrid formal framework serving as a ``model twin" for autonomous systems' safety verification. As a model twin, SOTERIA functions as an end-to-end digital twin for the target system, integrating both physical and computational aspects to facilitate comprehensive verification. By modeling the physical system's hybrid dynamics alongside the computational model and the operating environment, SOTERIA enables a rigorous safety assurance process that verifies both functional and temporal correctness. Using well-established verification tools, SOTERIA ensures that end-to-end latencies align with formal specifications, bridging the gap between computational and physical requirements. An extensive case study on the F1Tenth racing car demonstrates SOTERIA's capabilities, leveraging \uppaal to achieve superior results in worst-case latency and safe operational environments, yielding more verified safe racing tracks compared to conventional schedulability analyses. This digital twin-based approach underscores the importance of a cohesive verification strategy that enhances safety and reliability in autonomous systems.
Trigger-Based Discretization of Hybrid Games for Autonomous Cyber-Physical Systems
ABSTRACT. Hybrid games are a powerful framework for modelling interactions between cyber-physical systems (CPS). While their high level of nondeterminism allows the modelling of complex systems, it also makes many properties undecidable. This paper presents Hybrid Games with Triggers (HGT), an extension that reduces nondeterminism by embedding agents’ rational decision-making as triggers - conditions that, when met, prompt the agents to act. This approach leads to a time-abstract discrete game with a countable state space, where an agent has a winning strategy in the discrete game if and only if they do in the HGT. Our discretisation preserves both the continuous and discrete dynamics of the original hybrid game, providing a more structured, analysable model without sacrificing dynamic expressivity.
Falsification and Control of CPS using the Language Set of Discrete-Time Temporal Logic
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
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
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
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.
Intelligent Power Distribution Systems: Model, Utilization Bounds, and Implementation
ABSTRACT. Power Distribution Systems (PDSes) protect Cyber-Physical Systems from power faults. This work proposes an intelligent PDS with real-time current monitoring to improve fault tolerance. To bound the real-time workload, we define linear and nonlinear utilization bounding techniques unique to PDSes. We exploit sub-maximal loading inherent in all practical PDSes, providing a total system utilization bound less than the sum of individual task bounds. We show these techniques are safe and applicable to real PDSs. Simulation of existing and randomly generated PDSes show up to 90% utilization reduction versus a naive approach. An experimental, open-source PDS implementation is also provided to validate feasibility.
Mesh Network Scheduling based on Cyber-Physical Sensitivity for Wireless Control Systems
ABSTRACT. Wireless control systems (WCSs) are gaining rapid development in industrial automation. Compared to the star topology, mesh networks offer greater compatibility for large-scale applications that require high reliability, scalability, and extended coverage. In WCSs, multiple control loops share the multi-hop mesh network, leading to non-negligible and long-span communication latency in critical flows, which can severely degrade the overall control performance. Additionally, the criticality of each control flow largely depends on the features of the physical plant dynamics and the mesh network configuration, which is essential to properly and exactly represent. Moreover, the online scheduling and reconfiguration for large-scale mesh network for WCSs also pose unique challenges. In this paper, we propose a mesh network scheduling mechanism based on cyber-physical sensitivity. Firstly, we model each control loop as a switched system to represent the impact of arbitrary and fluctuating communication latency. Second, we propose a novel online criticality indicator, cyber-physical sensitivity (CP-Sensi), which accurately reflects the criticality of each control flow by synthesizing the switched model, run-time physical states, and network conditions. Finally, we design a CP-Sensi-based scheduling mechanism and an efficient piggyback-based network reconfiguration protocol tailored for mesh networks. Extensive studies with 12 control loops demonstrate that the proposed CP-Sensi and online mesh network scheduling achieve superior control performance compared to state-of-the-art approaches.
Analysis of Control Systems under Sensor Timing Misalignments
ABSTRACT. This paper presents an in-depth analysis of the stability and performance of control systems experiencing sensor timing misalignments, a common challenge in practical applications such as autonomous vehicles and aerospace systems. We model multichannel sensor delays as independent random variables, capturing the variability of real-world systems where different sensors exhibit distinct and nonconstant processing times or communication delays. This allows us to formulate the systems subject to delays as Markov Jump Linear Systems, enabling a rigorous examination of stability and performance under such misalignments. To validate the proposed methodology, we conduct experimental studies with two applications: an adaptive cruise controller and an inverted pendulum. In the analysis, we show that the impact of delays in different channels on a control system is typically not symmetric. Very often there is a sensor channel that is more critical for the controller and delays in that specific channel are hardly tolerated, while other channels can be delayed without compromising the stability and performance of the system.
ABSTRACT. With the increasing popularity of electric vehicles (EVs), drivers want their vehicle batteries to be charged in a few minutes; at present, this is feasible only if battery service stations replace the EV battery pack with a fully charged battery pack. In this paper, we formulate the scheduling problem for battery swap stations, aiming to provide the drivers with timing guarantees for different types of EVs, each with its own sporadic/periodic arrival pattern and deadline constraint. To solve the problem, we analyze its unique characteristics from a real-time scheduling perspective, with the main challenge being the circular timing dependency between two distinct scheduling processes: the swapping operation and the charging operation. We first derive a sufficient condition that decouples the dependency and then develop scheduling policies and timing guarantee techniques, designed for not only being specialized for the problem but also accommodating the sufficient condition in a time-predictable and resource-efficient manner. While the formulated problem and its solution hold significance as the first attempt to establish real-time scheduling principles for battery swap stations, we also propose strategies to accommodate real-world EV arrivals that do not necessarily follow a sporadic/periodic pattern. Finally, we evaluate the effectiveness of the proposed principles not only in addressing the target problem but also in accommodating real-world EV arrival patterns.
GPIoT: Tailoring Small Language Models for IoT Program Synthesis and Development
ABSTRACT. Code Large Language Models (LLMs) enhance software development efficiency by automatically generating code and documentation in response to user requirements. However, code LLMs cannot synthesize specialized programs when tasked with IoT applications that require domain knowledge. While Retrieval-Augmented Generation (RAG) offers a promising solution by fetching relevant domain knowledge, it necessitates powerful cloud LLMs (e.g., GPT-4) to process user requirements and retrieved contents, which raises significant privacy concerns. This approach also suffers from unstable networks and prohibitive LLM query costs. Moreover, it is challenging to ensure the correctness and relevance of the fetched contents. To address these issues, we propose GPIoT, a code generation system for IoT applications by fine-tuning locally deployable Small Language Models (SLMs) on IoT-specialized datasets. SLMs have smaller model sizes, allowing efficient local deployment and execution to mitigate privacy concerns and network uncertainty. Furthermore, by fine-tuning the SLMs with our IoT-specialized datasets, the SLMs' ability to synthesize IoT-related programs can be substantially improved. To evaluate GPIoT's capability in synthesizing programs for IoT applications, we develop a benchmark, IoTBench. Extensive experiments and user trials demonstrate the effectiveness of GPIoT in generating IoT-specialized code, outperforming state-of-the-art code LLMs with an average task accuracy increment of 64.7% and significant improvements in user satisfaction.
TaskSense: A Translation-like Approach for Tasking Heterogeneous Sensor Systems with LLMs
ABSTRACT. An increasing number of environments, such as smart homes and factories, are being equipped with multiple sensor systems to enable diverse intelligent applications. However, most existing sensor coordination systems require manually predefined rules, limiting their ability to handle flexible and complex tasks. While recent approaches leverage large language models (LLMs) to interact with external APIs, they struggle to fully understand the capabilities and data dependencies of practical sensor systems. This paper introduces TaskSense, a novel system that coordinates multiple sensor systems in response to users' complex queries. TaskSense introduces a sensor language that automatically translates the capabilities and data dependencies of sensor systems into vocabularies and grammar rules that can be understood by LLMs. It then interprets user intentions into executable task plans for sensor systems using this sensor language in combination with LLMs. Meanwhile, TaskSense checks the solvability of user queries and verifies the correctness of task plan dependencies. To further enhance robustness, TaskSense incorporates a dynamic plan execution mechanism that adjusts plans based on real-time feedback from sensor data availability, data quality and execution results. TaskSense is deployed on real-world smart home systems, utilizing six popular LLMs. The system is evaluated across 4 scenarios involving 9 types of sensor systems, over 60 APIs, 170 tasks and 5 types of data modalities. Results show that TaskSense achieves up to 2× higher planning accuracy and a 75% increase in answer accuracy using the similar amount of tokens compared with baseline approaches.
SelfReplay: Adapting Self-Supervised Sensory Models via Adaptive Meta-Task Replay
ABSTRACT. Self-supervised learning enables effective model pre-training on large-scale unlabeled data, which is crucial for user-specific fine-tuning in mobile sensing applications. However, pre-trained models often face significant domain shifts during fine-tuning due to user diversity, leading to performance degradation. To address this, we propose SelfReplay, an adaptive approach designed to align self-supervised models to different domains. SelfReplay consists of two stages: MetaSSL, which leverages meta-learning with self-supervised learning to pre-train domain-adaptive weights, and ReplaySSL, which further adapts the pre-trained model to each user's domain by replaying the meta-learned self-supervised task with a few user-specific samples. This produces a personalized model tailored to each user. Evaluations on mobile sensing benchmarks demonstrate that SelfReplay outperforms existing baselines, improving the F1-score by 9.4%p on average. On-device analyses on a commodity smartphone show the efficiency of SelfReplay's adaptation step, required just once after deployment, with SimCLR completing in only 10 seconds while using less than 100MB of memory.
Babel: A Scalable Pre-trained Model for Multi-Modal Sensing via Expandable Modality Alignment
ABSTRACT. This paper presents Babel, the expandable modality alignment model, specially designed for multi-modal sensing. While there has been considerable work on multi-modality alignment, they all struggle to effectively incorporate multiple sensing modalities due to the data scarcity constraints. How to utilize multi-modal data with partial pairings in sensing remains an unresolved challenge.
Babel tackles this challenge by introducing the concept of expandable modality alignment. The key idea involves transforming the N-modality alignment into a series of binary-modality alignments. Novel techniques are also proposed to further mitigate data scarcity issue and balance the contribution of the newly incorporated modality with the previously established modality alignment during the expandable alignment process. We provide the comprehensive implementation. In the pre-training phase, Babel currently aligns 6 sensing modalities, namely Wi-Fi, mmWave, IMU, LiDAR, video, and depth. For the deployment phase, as a foundation model, any single or combination of aligned modalities could be selected from Babel and applied to downstream tasks.
Evaluation demonstrates Babel's outstanding performance on eight human activity recognition datasets, compared to a broad range of baselines e.g., the SOTA single-modal sensing networks, multi-modal sensing framework, and multi-modal large language models. Babel not only improves the performance of individual modality sensing (12% averaged accuracy improvement), but also effectively fuses multiple available modalities (up to 22% accuracy increase). Case studies also highlight emerging application scenarios empowered by Babel, including cross-modality retrieval (i.e.,sensing imaging), and bridging LLMs for sensing comprehension.
Toward Sensor-In-the-Loop LLM Agent: Benchmarks and Implications
ABSTRACT. This paper explores sensor-informed personal agents that can take advantage of sensor hints on wearables to enhance the personal agent's response. We demonstrate that such a sensor-in-the-loop AI agent design can be easily integrated into existing LLM agents by building a prototype named WellMax based on existing well-developed techniques such as structured prompt templates and few-shot prompting. The head-to-head comparison with a non-sensor-informed agent across five use scenarios demonstrates that this sensor-in-the-loop design can effectively improve users' needs and their overall experience. The deep-dive into agents' replies and participants' feedback further reveals that sensor-in-the-loop agents not only provide more contextually relevant responses but also exhibit a better understanding of user priorities and situational nuances. In addition, we conduct two case studies to examine the potential pitfalls and distill key insights from this sensor-in-the-loop agent. We hope this work can spawn new ideas for building more intelligent, empathetic, and effective AI-driven personal assistants.
WixUp: A Generic Data Augmentation Framework for Wireless Human Tracking
ABSTRACT. Wireless sensing technologies, leveraging ubiquitous sensors such as acoustics or mmWave, can enable various applications such as human motion and health tracking. However, the recent trend of incorporating deep learning into wireless sensing introduces new challenges, such as the need for extensive training data and poor model generalization. As a remedy, data augmentation is one solution well-explored in other fields such as computer vision; yet they are not directly applicable due to the unique characteristics of wireless signals. Hence, we propose a custom data augmentation framework, WixUp, tailored for wireless human sensing. Our goal is to build a generic data augmentation framework applicable to various tasks, models, data formats, or wireless modalities. Specifically, WixUp achieves this by a custom Gaussian mixture and probability-based transformation, making any data formats capable of an in-depth augmentation at the dense range profile level.Additionally, our mixing-based augmentation enables unsupervised domain adaptation via self-training, allowing model training with no ground truth labels from new users or environments in practice.We extensively evaluated WixUp across four datasets of two sensing modalities (mmWave, acoustics), two model architectures, and three tasks (pose estimation, identification, action recognition). WixUp provides consistent performance improvement (2.79%-84.25%) across these various scenarios and outperforms other data augmentation baselines.
Successive Control Barrier Functions for Nonlinear Systems
ABSTRACT. We present the idea of successive control barrier functions for nonlinear (polynomial) control systems. Control Barrier Functions (CBFs) can be used to maintain safety properties for a system through the online modification of control inputs to ensure that the state remains inside a controlled invariant set that excludes a set of unsafe states. However, the synthesis of CBFs is quite difficult in practice, especially for nonlinear dynamical systems. Computationally inexpensive approaches employ relaxed control barrier conditions that result in relatively small control invariant sets. In turn, this can result in unnecessary modification of the nominal control input to keep the dynamics inside this set.
In this paper, we propose the concept of "successive" CBFs.Rather than rely on a single CBF, our approach uses a hierarchy of functions wherein functions at one level of a hierarchybecome active only if the functions at the previous levels have failed. Using a well-known approach to finding barrierfunctions for polynomial dynamical systems using sum of squares optimization, we show how to adapt it to synthesize successive barrier functions. We also provide "transit time" guarantees to construct a chattering-free runtime enforcement scheme that avoids collisions with fixed obstacles. We demonstrate our approach on a set of interesting nonlinearbenchmarks, while comparing it with state of the art approaches for synthesizing CBFs.
Certifying Lyapunov Stability of Black-Box Nonlinear Systems via Counterexample Guided Synthesis
ABSTRACT. Finding Lyapunov functions to certify the stability of control systems has been an important topic for certifying safety-critical systems. Most existing methods on finding Lyapunov functions require access to the dynamics of the system. Accurately describing the complete dynamics of a control system however remains highly challenging in practice. Latest trend of using learning-enabled control systems further reduces the transparency. Hence, a method for black-box systems would have much wider applications.
Our work stems from the idea of sampling and exploiting Lipschitz continuity to approximate the unknown dynamics. Given Lipschitz constants, one can derive a non-statistical upper bounds on approximation errors; hence a strong certification on this approximation can certify the unknown dynamics. We significantly improve this idea by directly approximating the Lie derivative of Lyapunov functions instead of the dynamics. We propose a framework based on the learner-verifier architecture from Counterexample-Guided Inductive Synthesis (CEGIS). Our insight of combining regional verification conditions and counterexample-guided sampling enables a guided search for samples to prove stability region-by-region. Our CEGIS algorithm further ensures termination.
Our numerical experiments suggest that it is possible to prove the stability of 2D and 3D systems with a few thousands of samples. In comparison with the existing black-box approach, our approach at the best case requires less than 0.01% of samples.
Polyhedral Control Lyapunov Functions for Switched Affine Systems
ABSTRACT. We present a counterexample-guided approach for synthesizing convex piecewise affine control Lyapunov functions, obtained as the maximumover a finite number of affine functions, for stabilizing switched linear systems. Our approachconsiders systems whose dynamics are defined by a set of affine ODEs over different regions of the state-space. The goal is to synthesize a control feedback functionthat uses state-based switching by assigning a dynamical mode to each state from the set of available dynamics. This is achieved by synthesizing a piecewise affinecontrol Lyapunov function that guarantees that for each state variable, the appropriate choice of a control input can cause an instantaneous decrease in the valueof the Lyapunov function. Since piecewise affine functions are not smooth, we use a non-smooth analytic characterization of piecewise affine Lyapunov functions.The key contribution of our approach is a counterexample driven algorithm that alternates between verification that a given convex PWA function is a control Lyapunovfunction or generating a counterexample point where the Lyapunov conditions fail, and synthesis from a finite set of counterexamples generated in the past.We demonstrate that the two steps can be performed using mixed integer linear programming problems (MILP) although no termination guarantees are possible. We show that the branch andcut approach used inside a MILP solver can be adapted to yield a termination guarantee. Although the resulting approach is computationally expensive, it has the advantage of not requiring a "demonstrator" or a pre-existing controller. We provide an empirical evaluation that explores the results of this approach over a set of numerical examples.
Psychophysiology-aided Perceptually Fluent Speech Analysis of Children Who Stutter
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
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
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.
Optimal Task Phasing for End-To-End Latency in Harmonic and Semi-Harmonic Automotive Systems
ABSTRACT. In the context of automotive systems, the end-to-end latency of a sequence of tasks (a so-called cause-effect chains) is a common metric to ensure correct timing behavior. To control the end-to-end latency, proper task configuration is crucial. While the literature considers the configuration of task periods, optimization of task phases to minimize the end-to-end latency is only sparsely discussed.
In this work, we discuss the configuration of task phases to optimize the end-to-end latency of a cause-effect chain that communicates under the Logical Execution Time (LET) paradigm. To that end, we develop a strategy for cause-effect chains with semi-harmonic periods, which are very common in industrial applications. We prove that our strategy is optimal in the sense that it minimizes the end-to-end latency. Furthermore, our evaluation based on a real-world use-case and on synthetic automotive benchmarks show that optimizing task phases can reduce end-to-end latencies significantly. Our approach takes at most 49us to find the optimal phasing and compute the end-to-end latency for cause-effect chains with 50 tasks, reducing the end-to-end latency by 28% in median.
Reconciling ROS 2 with Classical Real-Time Scheduling of Periodic Tasks
ABSTRACT. The Robot Operating System 2 (ROS 2) is a widely used middleware that provides software libraries and tools for developing robotic systems. In these systems, tasks are scheduled by ROS 2 executors. Since the scheduling behavior of the default ROS 2 executor is inherently different from classical real-time scheduling theory, dedicated analyses or alternative executors, requiring substantial changes to ROS 2, have been developed.
In 2023, the events executor was introduced into ROS 2. It features an events queue and allows the possibility to make scheduling decisions immediately after a job completes. In this paper, we show that, with very minor modifications of the events executor, a large body of research results from classical real-time scheduling theory becomes directly applicable for ROS 2. This enables analytical bounds on the worst-case response time and the end-to-end latency, outperforming bounds for the default ROS 2 executor in many scenarios. Our solution is easy to integrate into existing ROS 2 systems since it requires only minor modifications of the events executor, which is natively included in ROS 2. The evaluation results show that our ROS 2 events executor with minor modifications can have significant improvement in terms of dropped jobs, worst-case response time, end-to-end latency, and performance compared to the default ROS 2 executor.
Jointly Ensuring Timing Disparity and End-to-End Latency Constraints in Hybrid DAGs (Outstanding Paper Award)
ABSTRACT. Autonomous machines often encounter complex timing constraints, such as those concerning end-to-end timing guarantees and real-time data fusion, etc. Tasks are often activated at varying rates and exhibit data dependencies in between. %As a result, m Maintaining the real-time performance of autonomous machines becomes a highly challenging endeavor. In this paper, we formulate the workload of an autonomous machine as a hybrid Directed Acyclic Graph (DAG), with a distinct focus on the task of %simultaneously ensuring timing consistency in data fusion and adherence to end-to-end constraints within the hybrid DAG model. We design a concise mechanism to select suitable data received by a node and transmit them to successor nodes. This ensures both the timing disparity---as reflected by the differences in timestamps of the data used for fusion---and the end-to-end latency from the sensor to the controller is confined within a certain boundary. The proposed method is proven to be optimal as it always selects suitable data to guarantee the timing correctness of an autonomous machine as far as it (inherently) has the capacity. Experimental results show that our method can significantly improve the success rate of guaranteeing both timing consistency and end-to-end constraints of the autonomous machine.
CROS-RT: Cross-Layer Priority Scheduling for Predictable Inter-Process Communication in ROS 2 (Outstanding Paper Award)
ABSTRACT. The Robot Operating System 2 (ROS2) is a popular middleware for distributed robotic applications. However, achieving real-time guarantees in ROS2 is challenging due to unpredictable delays and priority inversions. We reveal that these issues arise from the lack of consistent priority propagation across ROS2’s multi-layered communication architecture, particularly down to the kernel layer. To address this, we present CROS-RT, the first cross-layer scheduler explicitly designed to tackle the unpredictability in ROS2 inter-process communication caused by multi-layer priority misalignment. CROS-RT ensures consistent, priority-based scheduling across the application, middleware, and kernel layers, introducing mechanisms for priority propagation, kernel-level message prioritization, and dynamic kernel thread adjustment. We have implemented and evaluated CROS-RT on the current stable release of ROS2. Experiments demonstrate that CROS-RT enhances communication predictability, reducing the worst-case response time by up to 89.3% over a baseline (vanilla ROS2). Additionally, we provide an analytical model to derive upper bounds on response times, ensuring reliable real-time performance for safety-critical applications.
Physics-Informed Mixed-Criticality Scheduling for F1Tenth Cars with Preemptable ROS 2 Executors
ABSTRACT. Autonomous systems are increasingly used in safety-critical domains, including industrial automation, autonomous vehicles, and the Industrial Internet of Things (IIoT). Verifying both the functional and temporal correctness of these systems is essential to ensure safety before deployment. However, end-to-end verification is challenging due to the interaction of continuous-time physical processes with discrete-time computational systems. Existing formal methods often assume simplified or static computational models, while traditional real-time systems focus on meeting timing constraints without explicitly linking them to physical safety. We address this gap by proposing a physics-informed, mixed-criticality (MC) verification framework for cyber-physical systems, which allows the integration of computational and physical models for dynamic, fine-grained safety assurance. Our framework incorporates feedback from the local environment to guide criticality-based mode switching, ensuring adaptive responses to real-time physical states rather than relying on global worst-case assumptions. We demonstrate the feasibility of our approach with a prototype implementation on an autonomous F1Tenth vehicle using ROS 2 and fully-preemptive EDF scheduling. Verification is conducted using UPPAAL to validate system behavior, mode transitions, and physical safety constraints. Results show that our framework effectively manages mixed-criticality requirements, enhancing responsiveness and safety in dynamic environments. Future work will focus on formal correctness proofs and additional real-world case studies.
SHADE-AD: An LLM-Based Framework for Synthesizing Activity Data of Alzheimer's Patients
ABSTRACT. Alzheimer's Disease (AD) has become an increasingly critical global health concern, which necessitates effective monitoring solutions in smart health applications. However, the development of such solutions is significantly hindered by the scarcity of AD-specific activity datasets. To address this challenge, we propose SHADE-AD, a Large Language Model (LLM) framework for Synthesizing Human Activity Datasets Embedded with AD features. Leveraging both public datasets and our own collected data from 99 AD patients, SHADE-AD synthesizes human activity videos that specifically represent AD-related behaviors. By employing a three-stage training mechanism, it broadens the range of activities beyond those collected from limited deployment settings. We conducted comprehensive evaluations of the generated dataset, demonstrating significant improvements in downstream tasks such as Human Activity Recognition (HAR) detection, with enhancements of up to 79.69%. Detailed motion metrics between real and synthetic data show strong alignment, validating the realism and utility of the synthesized dataset. These results underscore SHADE-AD's potential to advance smart health applications by providing a cost-effective, privacy-preserving solution for AD monitoring.
Multi-Modal Dataset Across Exertion Levels: Capturing Post-Exercise Speech, Breathing, and Phonocardiogram
ABSTRACT. Cardio exercise elevates both heart rate and respiration rate, resulting in distinct physiological changes that affect speech patterns, pitch, breathing sounds, and heart sounds. These variations, which occur post-exercise, are influenced by factors such as exercise intensity and individual fitness levels. A comprehensive audio dataset is critically needed to capture post-exercise physiological changes, as existing datasets focus mainly on resting speech, breathing, and heart sounds, neglecting the dynamic shifts following physical exertion. Current datasets fail to capture unique post-exercise variations like speech disfluencies, altered breathing patterns, and variable heart sound intensities, limiting model generalizability to post-exercise conditions. To address this gap, we recruited 46 subjects from diverse backgrounds to engage in cardio exercise, specifically running, reaching varied exertion levels to produce a rich dataset. Our dataset includes 228 sessions totaling 39 minutes of structured reading, 57 minutes of spontaneous speech, 62 minutes of breathing sounds, and 126 minutes of phonocardiogram (PCG) recordings. We designed and deployed preliminary case studies to show that speech changes post-cardio could serve as an indicator of exertion level. We envision this dataset as a foundational resource for designing models in speech and cardiorespiratory monitoring that are resilient to the physiological shifts induced by exercise. This dataset could advance natural language processing (NLP) applications and mobile health technologies by enabling resilient and accurate physiological monitoring in real-world conditions.
SensorQA: A Question Answering Benchmark for Daily-Life Monitoring
ABSTRACT. With the rapid growth in sensor data, effectively interpreting and interfacing with these data in a human-understandable way has become crucial. While existing research primarily focuses on learning classification models, fewer studies have explored how end users can actively extract useful insights from sensor data, often hindered by the lack of a proper dataset.
To address this gap, we introduce SensorQA, the first human-created question-answering (QA) dataset for daily life monitoring, based on long-term time-series sensor data. SensorQA is created by human workers and includes 5.6K diverse and practical queries that reflect genuine human interests, paired with accurate answers derived from the sensor data. We further establish benchmarks for state-of-the-art AI models on this dataset and evaluate their performance on typical edge devices. Our results reveal a gap between current models and optimal QA performance as well as efficiency, highlighting the need for new contributions. The dataset and code are available at: https://github.com/benjamin-reichman/SensorQA.
SEE-V2X: C-V2X Direct Communication Dataset: An Application-Centric Approach
ABSTRACT. Cellular-vehicle-to-everything (C-V2X) technology has been increasingly adopted by the research community, automotive industry, and government agencies as the next key technology to enhance transportation safety and efficiency. Recent years have also witnessed emerging C-V2X-based applications, connecting sensors on vehicle (V2V), from infrastructure (V2I), and carried by pedestrians (V2P), to enable novel capabilities such as cooperative perception, sustainable transportation, and remote operations. While researchers have made successful strides in simulating these promising applications, the disconnect with real-world C-V2X performance often renders ungrounded assumptions, resulting in huge barriers towards deployment. In this paper, we aim to build and release a real-world C-V2X dataset, SEE-V2X, using commercial off-the-shelf standard compliant C-V2X radios. Emulating the traffic patterns of popular C-V2X applications, we investigate the gap between the demand and reality. Beyond throughput and latency, SEE-V2X contains cross-layer details, offers insight into the resource scheduling and allocation mechanism in various situations, and reveals the impact of nuanced configuration. Our preliminary analysis shows that severe packet collision and jitter can easily happen, indicating opportunities to avoid performance degradation with careful and subtle configuration. SEE-V2X dataset and the analysis tools are available at https://cisl.ucr.edu/SEE-V2X-Dataset/.