Abstract: In October 2023, the Onboard Planner (OBP) took control of the Perseverance rover on Mars, over 200 million miles from Earth. As of 29th January 2025, OBP has operated for 429 Martian days (sols) and has: executed over 7800 activities requested by scientists and engineers, driven over 12 kilometers, acquired over 70,000 images, and collected 4 rock core samples. In contrast to the traditional form of operations, where operators provide a rigid set of instructions for the rover, with OBP Perseverance revises its schedule an average of 16 times each day to stay responsive in a dynamic Martian environment where things don’t always go as expected. This flexibility allows the mission to manage resources such as energy more efficiently and therefore accomplish more science.
In this talk, we discuss the approach to ensuring that a search-based AI system, specifically the Onboard Planner, would (1) achieve mission objectives; and critically (2) protect the rover, a multi-billion dollar one of a kind asset. We describe the “whole lifecycle” approach to developing trusted autonomy software for M2020, spanning: conception, design, analysis, prototyping, and testing. We then describe the incremental rollout and training to smooth the transition to operations with increased onboard autonomy. Next we discuss how the OBP software has performed. Finally we describe the even greater challenges of autonomy in future missions to hunt for life beyond Earth.
Bio: Steve Chien is a Technical Fellow in Artificial Intelligence and Co-head of the Artificial Intelligence Group at the Jet Propulsion Laboratory, California Institute of Technology. He has spent decades deploying AI/Autonomy to numerous space missions including: Earth Observing One, Sensorweb, ESA’s Rosetta Orbiter, and M2020. He has been awarded four NASA Medals in 1997, 2000, 2007, and 2015 for development and deployment of AI technologies for space missions. He has supported numerous government bodies including the Defense Science Board and the Air Force Scientific Advisory Board. He was appointed by Congress to the National Security Commission on Artificial Intelligence (2018-2021). He currently serves on the Army Science Board and as an Advisor to the Senate Defense Modernization Caucus.
Sparse Intersection Checking for Sparse Polynomial Zonotopes
ABSTRACT. Polynomial zonotopes are a non-convex set representation that have many applications, such as reachability analysis of hybrid systems, control in robotics, and verification of nonlinear systems. Such analysis methods often require intersection checking. The usual algorithm for intersection checking is to, first, overapproximate the polynomial zonotope by a zonotope and then, if the overapproximation is too large, split the set and recursively and repeat. Although the overapproximation error in this algorithm converges to the original polynomial zonotope, there are still two problems. First, the overapproximation error is not monotonically decreasing after each split. Second, more critically, the split polynomial zonotopes do not preserve the sparsity structure as the original polynomial zonotope, eliminating any memory and other efficiency benefits made possible by the sparse structure. In this paper, we propose a variation of polynomial zonotopes called \emph{denormalized polynomial zonotopes}, where each factor variable does not need to be in the range [-1, 1]. We prove this slight modification eliminates the two above issues, while still guaranteeing that overapproximation error will converge to the exact polynomial zonotope. We demonstrate the efficiency improvements through numerical experiments, where in certain cases denormalized polynomial zonotope intersectionchecking is over 400x faster and uses 550x less memory.
Indistinguishability in Localization and Control with Coarse Information
ABSTRACT. We study localization and control problems in which agent dynamics are described by difference or differential equations, while output measurements are collected at discrete times and given by finite-valued maps depending on possibly unknown landmark locations. Guided by the goal of understanding fundamental limitations imposed by such coarse measurements, we focus on characterizing indistinguishable states of the system, i.e., agent-landmark pairs that produce identical observations under all control inputs. We show that indistinguishability relations can be checked automatically under mild assumptions and, being a special type of bisimulation, we develop an iterative algorithm for approximately computing it. We then introduce an analytical approach, rooted in observability theory of linear control systems, which iteratively computes a sequence of subspaces converging in finitely many steps to the indistinguishable subspace; a differential-geometric extension to nonlinear systems is also outlined.
Stationary regimes of piecewise linear dynamical systems with priorities
ABSTRACT. Dynamical systems governed by priority rules appear in the modeling of emergency organizations and road traffic. These systems can be modeled by piecewise linear time-delay dynamics, specifically using Petri nets with priority rules. A central question is to show the existence of stationary regimes (i.e., steady state solutions)---taking the form of invariant half-lines---from which essential performance indicators like the throughput and congestion phases can be derived. Our primary result proves the existence of stationary solutions under structural conditions involving the spectrum of the linear parts within the piecewise linear dynamics. This extends a fundamental theorem due to Kohlberg (1980) from nonexpansive dynamics to a broader class of systems. The proof of our result relies on topological degree theory and the notion of "Blackwell optimality" from the theory of Markov decision processes. Finally, we validate our findings by demonstrating that these structural conditions hold for a wide range of dynamics, especially those stemming from Petri nets with priority rules, and we illustrate on real-world examples from road traffic management and emergency call center operations.
Sharc: Simulator for Hardware Architecture and Real-time Control
ABSTRACT. Tight coupling between computation, communication, and con-trol pervades the design and application of cyber-physical systems(CPSs). Due to the complexity of these systems, advanced designprocedures that account for these tight interconnections are para-mount to ensure the safe and reliable operation of control algo-rithms under computational constraints. In this paper, we presenta tool, called Simulator for Hardware Architecture and Real-timeControl (Sharc), to assist in the co-design of control algorithmsand the computational hardware on which they are run. Sharcsimulates a user-specified control algorithm on a user-specifiedmicroarchitecture, evaluating how computational constraints af-fect the performance of the control algorithm and the safety of thephysical system. We illustrate the power of Sharc by examiningan adaptive cruise control example and a cart-pole example.
Can control barrier functions keep automated vehicles safe in live freeway traffic?
ABSTRACT. This work presents testing of a Control Barrier Function (CBF) supervised Automated Vehicle (AV) in live freeway traffic. The CBF is designed and implemented using a common dynamical model for AV longitudinal control and a time-gap based safety property combined with CAN bus injection software/hardware. Over an hour of car-following data is collected from driving in congested freeway traffic. We analyze the extent to which the CBF controlled AV satisfied three properties: 1) forward-invariance of the safety property, 2) recovery of the safety property, and 3) collision avoidance.Our main findings are as follows. Forward-invariance was not strictly satisfied across all states. When trajectories begin satisfying the safety property it was violated by a maximum of 3.4 [m], and 90% of violations were less than 2 [m]. Recovery was also not strictly satisfied across all states. For trajectories which begin outside of the safe set due to merge-in events, if the violation to the safety property was by more than 5 [m] the AV was recovering back to the safe set in more than 98% of the time. Finally, the minimum spacing-gap was 11.7 [m]. Across the tests the AV remained far from any collisions. We additionally analyze errors between control inputs and achieved outputs and hypothesize that unaccounted for modeling errors may lead to under-braking compared to what the CBF logic specifies, which may contribute to the observed property violations.
Breaking the Latency Barrier: Practical Haptic Bilateral Teleoperation over 5G
ABSTRACT. Haptic bilateral teleoperation holds promise for applications such as telemaintenance, remote manipulation, and disaster response, yet delivering precise, low-latency force and video feedback remains challenging. This study advances haptic bilateral teleoperation by combining live video with Model Mediated Teleoperation (MMT) to enable predictive force feedback. A novel algorithm allows the robotic device to replicate interactions predictively experienced by the operator. We validated this approach in a fully functional system that performs reliably despite significant network delays. The latency performance of the system is extensively characterized, achieving a motion-to-pixel latency of 58 ms. A user study revealed that operators did not perceive network latency of at least 75 ms, resulting in a 133 ms motion-to-pixel delay requirement. Additionally, a 5G latency analysis demonstrated that effective haptic teleoperation is achievable with both operator and remote ends connected via 5G. This provides a path away from strict latency requirements toward practical teleoperation solutions using currently available technology.
Ethics by Design in Autonomous Driving: Developing a Model-Based Liability Determination Framework
ABSTRACT. Driving is a safety-critical activity, with most accidents caused by human errors. Advances in artificial intelligence (AI) offer the potential to reduce these errors, yet AI systems still face challenges in making socially acceptable decisions under complex and dynamic circumstances. To overcome these challenges, incorporating ethic-by-design principles is essential in developing autonomous systems. A crucial component of ethic-by-design is liability determination, which remains difficult to automate due to the need for retrospective analysis of vague and subjective criteria. In this paper, we propose a model-based liability determination framework that integrates legal doctrines with a driver behavior model. Our framework first formalizes liability determination based on established legal principles. The driver behavior model enables retrospective analysis by identifying reasonable alternative actions at each decision point, facilitating the assessment of duty breaches and proximate causes. We validate our framework through experiments focusing on highway driving accidents. We selected 8 representative simulated accidents and evaluated them with 5 senior traffic polices. The results demonstrate that our framework’s liability judgments closely align with those of the police, indicating high accuracy. Additionally, we examined the impact of breach of duty judgments on liability determination by utilizing Large Language Models (LLMs). The findings reveal that with only trajectories, LLM’s liability determinations were inaccurate, whereas incorporating these judgments resulted in outputs that matched police assessments. Our proposed liability determination framework effectively automates the process, providing accurate and interpretable results that support ethic-by-design in autonomous driving systems, thereby enhancing their safety and accountability.
From Systems to Hardware and Back: Unlocking the Potential of Cross-Layer Design
ABSTRACT. Abstract:
With the inevitable slowing of traditional CMOS scaling and the relentless rise of computational demands, it is increasingly clear that cross-layer design—also known in industry as system-technology co-design (STCO)—offers one of the most promising paths forward. This approach requires rethinking how we design computing systems, spanning across materials, devices, circuits, architectures, systems, software, and algorithms.
In this talk, I will reflect on my personal journey through this paradigm shift, highlighting key lessons and technical insights gained along the way. I will focus on how cross-layer design can be leveraged to address critical challenges such as the power wallandmemory wall in traditional von Neumann machines. The talk will show how embracing STCO can help us unlock new levels of efficiency and performance in future computing systems.
Bio:
Xiaobo Sharon Hu is Leo E. and Patti Ruth Linbeck Professor of Engineering in the department of Computer Science and Engineering at the University of Notre Dame, USA. She is currently working on a short-term assignment at the U.S. NSF as Program Director in the Division of Computing and Communication Foundations. Her research interests include low-power system design, circuit and architecture design with emerging technologies, real-time embedded systems, and hardware-software co-design. She has published more than 450 papers in these areas. Some of her recognitions include the Best Paper Award from the Design Automation Conference, International Conference on Computer-Aided Design, and the International Symposium on Low Power Electronics and Design; Marie R. Pistilli Women in Engineering Achievement Award; and NSF Career award. She served as the General Chair and/or TPC Chair of Design Automation Conference, Real-Time Systems Symposium, Embedded Systems Week, etc. She was the Editor-in-Chief of ACM Transactions on Design Automation of Electronic Systems and served as Associate Editor of other ACM and IEEE journals. Sharon Hu is a Fellow of the ACM and the IEEE.
Argus: Multi-View Egocentric Human Mesh Reconstruction Based on Stripped-Down Wearable mmWave Add-on
ABSTRACT. In this paper, we propose Argus, a wearable add-on system based on stripped-down (i.e., compact, lightweight, low-power, limited-capability) mmWave radars. It is the first to achieve egocentric human mesh reconstruction in a multi-view manner. Compared with conventional frontal-view mmWave sensing solutions, it addresses several pain points, such as restricted sensing range, occlusion, and the multipath effect caused by surroundings. To overcome the limited capabilities of the stripped-down mmWave radars (with only one transmit antenna and three receive antennas), we tackle three main challenges and propose a holistic solution, including tailored hardware design, sophisticated signal processing, and a deep neural network optimized for high-dimensional complex point clouds. Extensive evaluation shows that Argus achieves performance comparable to traditional solutions based on high-capability mmWave radars, with an average vertex error of 6.5 cm, solely using stripped-down radars deployed in a multi-view configuration. It presents robustness and practicality across conditions, such as with unseen users and different host devices.
Ultra-High-Frequency Harmony: mmWave Radar and Event Camera Orchestrate Accurate Drone Landing
ABSTRACT. For precise, efficient, and safe drone landings, ground platforms should real-time, accurately locate descending drones and guide them to designated spots. While mmWave sensing combined with cameras improves localization accuracy, the lower sampling frequency of traditional frame cameras compared to mmWave radar creates bottlenecks in system throughput. In this work, we replace the traditional frame camera with event camera, a novel sensor that harmonizes in sampling frequency with mmWave radar within the ground platform setup, and introduce mmE-Loc, a high-precision, low-latency ground localization system designed for drone landings. To fully leverage the temporal consistency and spatial complementarity between these modalities, we propose two innovative modules, consistency-instructed collaborative tracking and graph-informed adaptive joint optimization, for accurate drone measurement extraction and efficient sensor fusion. Extensive real-world experiments in landing scenarios from a leading drone delivery company demonstrate that mmE-Loc outperforms state-of-the-art methods in both localization accuracy and latency.
mmET: mmWave Radar-Based Eye Tracking on Smart Glasses
ABSTRACT. With the growing popularity of VR and AR devices, eye tracking has become a critical user interface and input modality for on-device AI agents. However, a compact, power-efficient, and robust eye tracking solution for AR/smart glasses remains an unsolved challenge. In this paper, we present mmET, the first mmWave radar-based eye tracking system on glasses. Our system, implemented as a pair of prototype glasses, utilizes sub-1cm mmWave radars placed near the eyes. The radars transmit FMCW signals and capture the reflections from the eyes and surrounding skin as the system input. To refine gaze estimation accuracy and data efficiency, we propose several novel methods: (1) concatenating multiple chirps and beamforming with learnable weights to improve resolution, (2) a novel neural network architecture to enhance robustness against remounting, (3) pretraining with contrastive loss to enable fast adaptation for new users. Experiments with 16 participants show that mmET achieves an average angular gaze direction error of 1.49∘ within sessions and 4.47∘ across remounting sessions, and reduces the training data needed for new users by 80% using the pretrained model.
Proteus: Enhanced mmWave Leaf Wetness Detection with Cross-Modality Knowledge Transfer
ABSTRACT. Accurate leaf wetness detection is essential to understanding plant health and growth conditions. The mmWave radar, with its sensitivity to subtle changes, is well-suited for leaf wetness detection. Existing mmWave-based approaches utilize the Synthetic Aperture Radar (SAR) algorithm to generate image-like inputs and rely on multi-modality fusion with an RGB camera to classify leaf wetness. However, the lack of understanding of SAR-based mmWave imaging limits its accuracy in various environments. This paper presents Proteus, a novel way of understanding mmWave SAR imaging. It includes an informative mmWave imaging processing system for accurate leaf wetness detection and duration measurement. We design a noise reduction algorithm to reduce speckle noise and improve image clarity for SAR-based mmWave imaging. Then, we incorporate phase angle data to enrich SAR texture information to capture high-resolution surface details, increasing informative features for precise wetness assessment in complex plant structures. Additionally, we introduce a cross-modality Teacher-Student network, using an RGB-based teacher model to guide the mmWave SAR-based student model for feature extraction. This network transfers the explicit knowledge in the RGB image domain to the mmWave image domain. We use commercial-off-the-shelf mmWave radar to prototype Proteus. The evaluation results show that Proteus achieves up to 96.% accuracy across varied environmental scenarios, outperforming state-of-the-art methods.
Improving mmWave based Hand Hygiene Monitoring through Beam Steering and Combining Techniques
ABSTRACT. We introduce BeaMsteerX (BMX), a novel mmWave hand hygiene gesture recognition technique that improves accuracy in longer ranges (1.5m). BMX steers a mmWave beam towards multiple directions around the subject, generating multiple views of the gesture that are then intelligently combined using deep learning to enhance gesture classification. We evaluated BMX using off-the-shelf mmWave radars and collected a total of 7,200 hand hygiene gesture data from 10 subjects performing a 6-step hand-rubbing procedure, as recommended by the World Health Organization, using sanitizer, at 1.5m—over 5 times longer than in prior works. BMX outperforms state-of-the-art approaches by 31-43% and achieves 91% accuracy at boresight by combining only two beams, demonstrating superior gesture classification in low SNR scenarios. BMX maintained its effectiveness even when the subject was positioned 30 degree away from the boresight, exhibiting a modest 5% drop in accuracy.
Composition of Constraints in Long Duration Autonomy
ABSTRACT. When robots are to be deployed over long time scales, optimality should take a backseat to “survivability”. In other words, it is more important that the robots do not experience mission-ending failures, such as collisions or complete depletion of their energy sources, rather than that they perform certain tasks as effectively as possible. For example, in the context of multi-agent robotics, we have a fairly good understanding of how to design coordinated control strategies for making teams of mobile robots achieve geometric objectives, such as assembling shapes or covering areas. But, what happens when these geometric objectives no longer matter all that much? In this talk, we consider this question of long duration autonomy for teams of robots that are deployed in an environment over a sustained period of time and that can be recruited to perform a number of different tasks in a distributed, safe, and provably correct manner. Survival will be encoded through Boolean composition of barrier functions. But, as these operations are non-differentiable, a non-smooth barrier function machinery is needed to manage the resulting complex, hybrid system dynamics.
Perception-based Quantitative Runtime Verification for Learning-enabled Cyber-Physical Systems
ABSTRACT. This paper proposes a perception-based quantitative approach to verify the safety of learning-enabled Cyber-Physical Systems (Le-CPS) at runtime. The proposed approach is developed based on probstar reachability, a new quantitative verification method for deep neural networks. It has two main components: perception-based runtime modeling and runtime quantitative verification. The perception-based runtime modeling method uses a probabilistic perception network to estimate the poses (modeled as a multivariate normal distribution) of moving obstacles. We transform sensing, actuating, and perception uncertainties into probabilistic initial conditions for the system’s states. The system model and initial conditions serve as inputs to a runtime reachability analysis algorithm, which constructs the system’s reachable sets for a short future horizon. These reachable sets are then used to quantitatively verify the system’s safety violation probability in real time. Our approach has been successfully deployed and validated on a real learning-based F1Tenth testbed with multiple autonomous driving scenarios, demonstrating its potential for enhancing the safety and reliability of autonomous systems. The reachable sets are used to quantitatively verify the safety violation probability of the system at runtime.
Safety Monitoring for Learning-Enabled Cyber-Physical Systems in Out-of-Distribution Scenarios
ABSTRACT. The safety of learning-enabled cyber-physical systems is hindered by the well-known vulnerabilities of deep neural networks to out-of-distribution (OOD) inputs. Existing literature has sought to monitor the safety of such systems by detecting OOD data. However, such approaches have limited utility, as the presence of an OOD input does not necessarily imply the violation of a desired safety property. We instead propose to directly monitor safety in a manner that is itself robust to OOD data. To this end, we predict violations of signal temporal logic safety specifications based on predicted future trajectories. Our safety monitor additionally uses a novel combination of adaptive conformal prediction and incremental learning. The former obtains probabilistic prediction guarantees even on OOD data, and the latter prevents overly conservative predictions. We evaluate the efficacy of the proposed approach in two case studies on safety monitoring: 1) predicting collisions of an F1Tenth car with static obstacles, and 2) predicting collisions of a race car with multiple dynamic obstacles. We find that adaptive conformal prediction obtains theoretical guarantees where other uncertainty quantification methods fail to do so. Additionally, combining adaptive conformal prediction and incremental learning for safety monitoring achieves high recall and timeliness while reducing loss in precision. We achieve these results even in OOD settings and outperform alternative methods.
Mining Specifications for Predictive Safety Monitoring
ABSTRACT. Safety-critical autonomous systems must reliably predict unsafe behavior to take timely corrective actions. Safety properties are often defined over variables that are not directly observable at runtime, making prediction and detection of violations hard. We present a new approach for learning interpretable monitors characterized by concise Signal Temporal Logic (STL) formulas that can predict safety property violations from the observable sensor data. We train these monitors from synthetic, possibly highly unbalanced data generated in a simulation environment. Our specification mining procedure combines a grammar-based method and two novel ensemble techniques. Our approach outperforms the existing solutions by enhancing accuracy and explainability, as demonstrated in two autonomous driving case studies.
Scalable and Interpretable Verification of Image-based Neural Network Controllers for Autonomous Vehicles
ABSTRACT. Existing formal verification methods for image-based neural network controllers in autonomous vehicles often struggle with high-dimensional inputs, computational inefficiency, and a lack of explainability. These challenges make it difficult to ensure safety and reliability, as processing high-dimensional image data is computationally intensive and neural networks are typically treated as black boxes. To address these issues, we propose SEVIN (Scalable and Explainable Verification of Image-Based Neural Network Controllers), a framework that leverages a Variational Autoencoders (VAE) to encode high-dimensional images into a lower-dimensional, explainable latent space. By annotating latent variables with corresponding control actions, we generate convex polytopes that serve as structured input spaces for verification, significantly reducing computational complexity and enhancing scalability. Integrating the VAE’s decoder with the neural network controller allows for formal and robustness verification using these explainable polytopes. Our approach also incorporates robustness verification under real-world perturbations by augmenting the dataset and retraining the VAE to capture environmental variations. Experimental results demonstrate that SEVIN achieves efficient and scalable verification while providing explainable insights into controller behavior, bridging the gap between formal verification techniques and practical applications in safety-critical systems.
Asymptotically Optimal Multiprocessor Real-Time Locking for non-JLFP Scheduling (Outstanding Paper Award)
ABSTRACT. In prior work, a number of asymptotically optimal suspension-based real-time locking protocols have been presented for job-level fixed priority (JLFP) schedulers, where job priorities do not change. However, the optimality proofs for these locking protocols break down under non-JLFP scheduling, where job priorities can vary. In fact, the problem of designing an asymptotically optimal real-time locking protocol for general non-JLFP scheduling has remained open. This paper closes this problem by presenting the non-JLFP locking protocol (NJLP), the first asymptotically optimal suspension-based real-time locking protocol for non-JLFP schedulers.
SPR: Shielded Processor Reservations with Bounded Management Overhead
ABSTRACT. With the increasing trend of hardware consolidation in modern computational infrastructures, ensuring predictable CPU allocation has become increasingly critical. Processor reservations, usually realized through rate-limiting servers, play an essential role in providing such predictability by enforcing CPU reservations. In theory, rate-limiting servers provide strong temporal isolation, meaning that a task’s timely access to its guaranteed budget is not contingent on the behavior of any other task in the system. However, in practice, these guarantees are brittle and easily undermined by the realities of actual hardware and shortcomings in naı̈ve reservation implementations. When confronted with malicious tasks using the reservation policy itself to attack the very security and rate properties it is meant to uphold, temporal isolation breaks down. In response, this paper presents Shielded Processor Reservation (SPR) scheduling, a novel approach that ensures that exactly one, and only one reservation is processed per scheduler invocation. SPR integrates deferred timer handling, early replenishment processing, processor access granularity guarantees, and bounded reservation management to provide robust temporal isolation. We implement SPR and existing rate-limiting servers in the Composite operating system and evaluate its performance. The results demonstrate that SPR not only provides reliable rate- limiting with low overhead but also mitigates vulnerabilities that can be exploited to attack existing reservation systems.
ABSTRACT. In real-time systems, handling tasks with highly variable computation times, some requiring parallel execution, poses significant scheduling challenges, particularly in maintaining low deadline miss rates without overprovisioning resources. This issue arises in applications like nonlinear optimization for Model Predictive Control (MPC).
The Constant Bandwidth Server (CBS) provides timing isolation, supporting both hard and soft real-time tasks. However, scheduling parallel, time-varying jobs across multiple CBS instances requires static job-to-server assignments, which can lead to resource underutilization due to queued jobs awaiting specific servers.
This paper introduces the Job Acceptance Multi-Server (JAMS), a mechanism in which multiple CBS instances share a common job queue, enabling flexible resource allocation for parallel workloads. JAMS incorporates a job dismissal mechanism to address overloads, ensuring that only jobs with guaranteed resource availability are accepted. Each CBS instance checks if it can complete a job by its deadline, given probabilistic knowledge on its execution times, dismissing unfeasible jobs to avoid excessive tardiness across queued tasks.
Implemented in Linux, JAMS is evaluated with computation times drawn from an MPC task and synthetic datasets. The extensive experimental results we provide demonstrate that JAMS effectively controls the deadline miss rate, maintaining it below a specified design threshold
Optimal Priority Assignment for Synchronous Harmonic Tasks With Dynamic Self-Suspension
ABSTRACT. Self-suspension behavior happens when a job has to wait for some activity to complete and results in substantial schedulability degradation in real-time systems. Despite extensive studies for self-suspending real-time task systems, the state of the art has barely addressed the optimality of the scheduling algorithms, especially for tasks with dynamic self-suspension.
In this paper, we explore optimal priority assignment for periodic real-time tasks with dynamic self-suspension under Task-level Fixed-Priority (T-FP) scheduling. To that end, we provide exact schedulability tests for frame-based and synchronous harmonic tasks. We show that the Suspension-Aware Deadline-Monotonic (SADM) priority assignment is an optimal fixed-priority scheduler for many scenarios. Further, for cases where SADM is not optimal, we adopt Audsley's Optimal Priority Assignment (OPA) approach to derive an optimal fixed-priority assignment. Evaluation results show that the exact tests outperform state-of-the-art schedulability tests from the literature, and that optimal priority assignments significantly improve schedulability over classical priority assignments.
ABSTRACT. Batteryless IoT systems face energy constraints exacerbated by checkpointing overhead. Approximate computing offers solutions but demands manual expertise, limiting scalability. This paper presents CheckMate, an automated framework leveraging LLMs for context-aware code approximations. CheckMate integrates validation of LLM-generated approximations to ensure correct execution and employs Bayesian optimization to fine-tune approximation parameters autonomously, eliminating the need for developer input. Tested across six IoT applications, it reduces power cycles by up to 60% with an accuracy loss of just 8%, outperforming semi-automated tools like ACCEPT in speedup and accuracy. CheckMate’s results establish it as a robust, user-friendly tool and a foundational step toward automated approximation frameworks for intermittent computing.
ABSTRACT. Internet-of-Things (IoT) devices are increasingly common in both consumer and industrial settings, often performing safety-critical functions. Although securing these devices is vital, manufacturers typically neglect security issues or address them as an afterthought. This is of particular importance in IoT networks, e.g., in the industrial automation settings.
To this end, network attestation – verifying the software state of all devices in a network – is a promising mitigation approach. However, current network attestation schemes have certain shortcomings: (1) lengthy TOCTOU (Time-Of-Check-Time-Of-Use) vulnerability windows, (2) high latency and resource overhead, and (3) susceptibility to interference from compromised devices. To address these limitations, we construct TRAIN (TOCTOU-Resilient Attestation for IoT Networks), an efficient technique that minimizes TOCTOU windows, ensures constant-time per-device attestation, and maintains resilience even with multiple compromised devices. We demonstrate TRAIN’s viability and evaluate its performance via a fully functional and publicly available prototype.
SecureGaze: Defending Gaze Estimation Against Backdoor Attacks
ABSTRACT. Gaze estimation models are widely used in applications such as driver attention monitoring and human-computer interaction. While many methods for gaze estimation exist, they rely heavily on data-hungry deep learning to achieve high performance. This reliance often forces practitioners to harvest training data from unverified public datasets, outsource model training, or rely on pre-trained models. However, such practices expose gaze estimation models to backdoor attacks. In such attacks, adversaries inject backdoor triggers by poisoning the training data, creating a backdoor vulnerability: the model performs normally with benign inputs, but produces manipulated gaze directions when a specific trigger is present. This compromises the security of many gaze-based applications, such as causing the model to fail in tracking the driver's attention. To date, there is no defense that addresses backdoor attacks on gaze estimation models. In response, we introduce SecureGaze, the first solution designed to protect gaze estimation models from such attacks. Unlike classification models, defending gaze estimation poses unique challenges due to its continuous output space and globally activated backdoor behavior. By identifying distinctive characteristics of backdoored gaze estimation models, we develop a novel and effective approach to reverse-engineer the trigger function for reliable backdoor detection. Extensive evaluations in both digital and physical worlds demonstrate that SecureGaze effectively counters a range of backdoor attacks and outperforms seven state-of-the-art defenses adapted from classification models.
Membership Inference Against Self-supervised IMU Sensing Applications
ABSTRACT. Deep learning has revolutionized the use of inertial measurement unit (IMU) sensors in mobile applications, such as human activity recognition. Building on the success of pre-trained models across various domains, recent studies have increasingly adopted self-supervised learning (SSL) for a range of sensing tasks. While these SSL approaches improve generalization and reduce labeling requirements, their privacy implications have received limited attention. This paper addresses this gap by examining IMU data privacy during pre-training through membership inference. Our work serves two important purposes: First, it enables data owners to verify if their data was used without permission in encoder pre-training. Second, it demonstrates how adversaries might compromise sensitive human sensing data used in pre-training. To enhance the practicality of membership inference on unlabeled IMU sensing data across different SSL algorithms, we introduce an activity labeling module and a novel perturbation strategy to exploit encoder overfitting characteristics on training data. When an encoder overfits, it memorizes training data rather than learning generalizable patterns. Therefore, when comparing the original data to the perturbed version, the encoder generates more distinct feature vectors for samples from its training set than for samples it has never seen before. We evaluate our membership inference methods on two mainstream SSL methods across multiple datasets, demonstrating that our method can achieve relatively high precision and recall at low false positive rates.
Poster Abstract: PRoTECT: Parallel Construction of Barrier Certificates for Safety Verification of Polynomial Systems, Ben Wooding, Viacheslav Horbanov and Abolfazl Lavaei
Poster Abstract: Physics-Informed Safety Verification of Nonlinear Systems: A Scenario Approach with Data Mitigation, Mohammadhossein Ashoori, Ali Aminzadeh, Abolfazl Lavaei and Amy Nejati
Poster Abstract: Verifying Vision-Based Autonomy with Abstract Rendering and Perception Contracts, Yangge Li, Chenxi Ji and Sayan Mitra
Poster Abstract: A gray box approach for Large Language Model-guided Natural Language to Temporal Logic Automatic, Eshita Shukla, Quinn Thibeault and Giulia Pedrielli
Poster Abstract: Symbolic Gaussian Smoothing, Andrew Mata, Ali Arjomandbigdeli and Stanley Bak
Poster Abstract: Polynomial Zonotopes Intersection Checking, Ertai Luo, Yushen Huang, Yifan Sun and Stanley Bak
Detection
Demo Abstract: SEQUIN: A Network Science and Physics-based Approach to Identify Sequential N-k Attacks in Electric Power Grids, Andrew Chio, Russell Bent, Kaarthik Sundar and Nalini Venkatasubramanian
Poster Abstract: Monitor and Recover: A Paradigm for Future Research on Distribution Shift in Learning-Enabled Cyber-Physical Systems, Vivian Lin and Insup Lee
Poster Abstract: Conformance-Driven Anomaly Detection for Cyber-Physical Systems, Xin Qin
Poster Abstract: Integrating the Simplex Architecture to Enhance Safety in Deep Learning Autonomous Systems, Niko Salamini, Federico Nesti, Mauro Marinoni, Giorgiomaria Cicero, Gabriele Serra, Alessandro Biondi and Giorgio Buttazzo
Demo Abstract: Real-Time Freeway Traffic Anomalous Event Detection System via Radar Detector Sensors, Austin Coursey, Junyi Ji, Zhiyao Zhang, William Barbour, Marcos Quinones-Grueiro, Tyler Derr, Gautam Biswas and Daniel Work
Poster Abstract: Data Efficient PV based Indoor Event Detection, Tushar Routh, Jiechao Gao and Bradford Campbell
Poster Abstract: Detecting Stealthy False Data Injections on Cyber-Physical Systems using Temporal Distance Metrics, Akash Bhattacharya, Suraj Singh, Sunandan Adhikary and Soumyajit Dey
Simulation
Poster Abstract: Adaptive Beamforming for Connected Vehicles – A Co-simulation Framework, Anik Roy, Varuni Reddy, Somnath Hazra, Serene Banerjee, Arnab Sarkar and Soumyajit Dey
Poster Abstract: 1000DaySim: Open-Source Traffic Simulation With Real Data Over Long Time Horizons, Zhiyao Zhang, Yuhang Zhang, Marcos Quiñones-Grueiro, William Barbour, Gautam Biswas and Daniel Work
Poster Abstract: Reproducible and Low-cost Sim-to-real Environment for Traffic Signal Control, Yiran Zhang, Khoa Vo, Longchao Da, Tiejin Chen, Xiaoou Liu and Hua Wei
Poster Abstract: SPHERE CPS: A Reconfigurable Testbed for Industrial Control System Security Experimentation, Luis Garcia, Jelena Mirkovic, David Balenson, Erik Kline, David Choffnes, Daniel Dubois, Srivatsan Ravi, Joseph Barnes, George Pradkin, Geoff Lawler, Chris Tran and Alba Regalado
Poster Abstract: Exploring Flexible Road Reconstruction in Godot Simulator, Daniel Peralta and Xin Qin
Poster Abstract: High-Level Scenario Management For Parallel Autonomous Vehicle Simulation, Alex Richardson and Jonathan Sprinkle
Demo Abstract: Cost-Effective Rover for Farms, Pawan Kumar, Yejur Dube and Hokeun Kim
Journal-first: Minimal-Overlap Centrality for Multi-Gateway Designation in Real-Time TSCH Networks. Authors: M. Gutiérrez Gaitán, L. Almeida, P. Santos, P. d’Orey, T. Watteyne
Work in Progress: Reducing WCET Estimation by Increasing the Number of Persistent Blocks. Authors: B. Geller, K. Rainey, C. Tessler, P. Modekurthy
Work in Progress: Security-Aware Preemptive Scheduling with Partial Trust for Safety-Critical Embedded Systems. Authors: F. Raadia, N. Fisher
Work in Progress: Biologically Inspired Dynamic Task Prioritization in Computer Vision Systems. Authors: J. Easton-Marks, A. Munoz, A. Cheng
Journal-first: A Machine Learning-based Platform for Monitoring and Prediction of Hazardous Gases in Rural and Remote Areas. Authors: E. Ladeira, B. Silva
Work in Progress: Self Healing Architectures Using Machine Learning and Federated Learning for Attack Detection. Authors: H. Ibrahim, H. Alkhzaimi
Brief Industry Paper: STM: A Static Non-preemptive Scheduler for NVIDIA Tegra SoC. Authors: A. Davies, N. Poorswani, R. Xiang, B. Brown, R. Singh, A. Tadkase, S. Gupta, A. Vafaee, J. Han, P. Tumati, S. Janapareddy
Work in Progress: Optimizing Schedulability using Cache-Bypassing. Authors: T. Fischer, H. Falk
Work in Progress: Increasing Schedulability via on-GPU Scheduling. Authors: J. Bakita, J. Anderson
Work in Progress: Middleware-transparent Callback Enforcement in Commoditized Component-oriented Real-time Systems. Authors: T. Ishikawa-Aso, A. Yano, T. Azumi, S. Kato
Journal-First: Cache-Related Preemption Delay in Non-Inclusive Cache Hierarchies. Authors: T. Fischer, H. Falk