Open Access. Powered by Scholars. Published by Universities.^{®}

Articles **1** - **21** of ** 21**

## Full-Text Articles in Engineering

Synthesizing Stealthy Reprogramming Attacks On Cardiac Devices, Nicola Paoletti, Zhihao Jiang, Ariful Islam, Houssam Abbas, Rahul Mangharam, Shan Lin, Zachary Gruber, Scott A. Smolka

#### Synthesizing Stealthy Reprogramming Attacks On Cardiac Devices, Nicola Paoletti, Zhihao Jiang, Ariful Islam, Houssam Abbas, Rahul Mangharam, Shan Lin, Zachary Gruber, Scott A. Smolka

*Real-Time and Embedded Systems Lab (mLAB)*

An Implantable Cardioverter Defibrillator (ICD) is a medical device used for the detection of potentially fatal cardiac arrhythmias and their treatment through the delivery of electrical shocks intended to restore normal heart rhythm. An ICD reprogramming attack seeks to alter the device’s parameters to induce unnecessary therapy or prevent required therapy. In this paper, we present a formal approach for the synthesis of ICD reprogramming attacks that are both effective, i.e., lead to fundamental changes in the required therapy, and stealthy, i.e., are hard to detect. We focus on the discrimination algorithm underlying Boston Scientific devices (one ...

Technical Report: Anytime Computation And Control For Autonomous Systems, Yash Vardhan Pant, Houssam Abbas, Kartik Mohta, Rhudii A. Quaye, Truong X. Nghiem, Joseph Devietti, Rahul Mangharam

#### Technical Report: Anytime Computation And Control For Autonomous Systems, Yash Vardhan Pant, Houssam Abbas, Kartik Mohta, Rhudii A. Quaye, Truong X. Nghiem, Joseph Devietti, Rahul Mangharam

*Real-Time and Embedded Systems Lab (mLAB)*

The correct and timely completion of the sensing and action loop is of utmost importance in safety critical autonomous systems. A crucial part of the performance of this feedback control loop are the computation time and accuracy of the estimator which produces state estimates used by the controller. These state estimators, especially those used for localization, often use computationally expensive perception algorithms like visual object tracking. With on-board computers on autonomous robots being computationally limited, the computation time of a perception-based estimation algorithm can at times be high enough to result in poor control performance. In this work, we develop ...

Holistic Resource Allocation For Multicore Real-Time Systems, Meng Xu, Linh T.X. Phan, Hyon-Young Choi, Yuhan Lin, Haoran Li, Chenyang Lu, Insup Lee

#### Holistic Resource Allocation For Multicore Real-Time Systems, Meng Xu, Linh T.X. Phan, Hyon-Young Choi, Yuhan Lin, Haoran Li, Chenyang Lu, Insup Lee

*Departmental Papers (CIS)*

This paper presents CaM, a holistic cache and memory bandwidth resource allocation strategy for multicore real-time systems. CaM is designed for partitioned scheduling, where tasks are mapped onto cores, and the shared cache and memory bandwidth resources are partitioned among cores to reduce resource interferences due to concurrent accesses. Based on our extension of LITMUS^{RT} with Intel’s Cache Allocation Technology and MemGuard, we present an experimental evaluation of the relationship between the allocation of cache and memory bandwidth resources and a task’s WCET. Our resource allocation strategy exploits this relationship to map tasks onto cores, and to ...

Data-Driven Model Predictive Control Using Random Forests For Building Energy Optimization And Climate Control, Francesco Smarra, Achin Jain, Tullio De Rubeis, Dario Ambrosini, Alessandro D'Innocenzo, Rahul Mangharam

#### Data-Driven Model Predictive Control Using Random Forests For Building Energy Optimization And Climate Control, Francesco Smarra, Achin Jain, Tullio De Rubeis, Dario Ambrosini, Alessandro D'Innocenzo, Rahul Mangharam

*Real-Time and Embedded Systems Lab (mLAB)*

Model Predictive Control (MPC) is a model-based technique widely and successfully used over the past years to improve control systems performance. A key factor prohibiting the widespread adoption of MPC for complex systems such as buildings is related to the difficulties (cost, time and effort) associated with the identification of a predictive model of a building. To overcome this problem, we introduce a novel idea for predictive control based on historical building data leveraging machine learning algorithms like regression trees and random forests. We call this approach Data-driven model Predictive Control (DPC), and we apply it to three different case ...

Data-Driven Switched Affine Modeling For Model Predictive Control, Francesco Smarra, Achin Jain, Rahul Mangharam, Alessandro D'Innocenzo

#### Data-Driven Switched Affine Modeling For Model Predictive Control, Francesco Smarra, Achin Jain, Rahul Mangharam, Alessandro D'Innocenzo

*Real-Time and Embedded Systems Lab (mLAB)*

Model Predictive Control (MPC) is a well-consolidated technique to design optimal control strategies, leveraging the capability of a mathematical model to predict the system’s behavior over a predictive horizon. However, building physics-based models for large-scale systems, such as buildings and process control, can be cost and time prohibitive. To overcome this problem we propose in this paper a methodology to exploit machine learning techniques (i.e. regression trees and random forests) in order to build a state-space switched affine dynamical model of a large scale system only using historical data. Finite Receding Horizon Control (RHC) setup using control-oriented data-driven ...

Parameter Invariant Monitoring For Signal Temporal Logic, Nima Roohi, Ramneet Kaur, James Weimer, Oleg Sokolsky, Insup Lee

#### Parameter Invariant Monitoring For Signal Temporal Logic, Nima Roohi, Ramneet Kaur, James Weimer, Oleg Sokolsky, Insup Lee

*Departmental Papers (CIS)*

*Signal Temporal Logic* (STL) is a prominent specification formalism for real-time systems, and monitoring these specifications, specially when (for different reasons such as learning) behavior of systems can change over time, is quite important. There are three main challenges in this area: (1) full observation of system state is not possible due to noise or nuisance parameters, (2) the whole execution is not available during the monitoring, and (3) computational complexity of monitoring continuous time signals is very high. Although, each of these challenges has been addressed by different works, to the best of our knowledge, no one has addressed ...

Fly-By-Logic: Control Of Multi-Drone Fleets With Temporal Logic Objectives, Yash Vardhan Pant, Houssam Abbas, Rhudii A. Quaye, Rahul Mangharam

#### Fly-By-Logic: Control Of Multi-Drone Fleets With Temporal Logic Objectives, Yash Vardhan Pant, Houssam Abbas, Rhudii A. Quaye, Rahul Mangharam

*Real-Time and Embedded Systems Lab (mLAB)*

The problem of safe planning and control for multi- drone systems across a variety of missions is of critical impor- tance, as the scope of tasks assigned to such systems increases. In this paper, we present an approach to solve this problem for multi-quadrotor missions. Given a mission expressed in Signal Temporal Logic (STL), our controller maximizes robustness to generate trajectories for the quadrotors that satisfy the STL spec- ification in continuous-time. We also show that the constraints on our optimization guarantees that these trajectories can be tracked nearly perfectly by lower level off-the-shelf position and attitude controllers. Our approach ...

Learning And Control Using Gaussian Processes, Achin Jain, Truong X Nghiem, Manfred Morari, Rahul Mangharam

#### Learning And Control Using Gaussian Processes, Achin Jain, Truong X Nghiem, Manfred Morari, Rahul Mangharam

*Real-Time and Embedded Systems Lab (mLAB)*

Building physics-based models of complex physical systems like buildings and chemical plants is extremely cost and time prohibitive for applications such as real-time optimal control, production planning and supply chain logistics. Machine learning algorithms can reduce this cost and time complexity, and are, consequently, more scalable for large-scale physical systems. However, there are many practical challenges that must be addressed before employing machine learning for closed-loop control. This paper proposes the use of Gaussian Processes (GP) for learning control-oriented models: (1) We develop methods for the optimal experiment design (OED) of functional tests to learn models of a physical system ...

Parameter-Invariant Monitor Design For Cyber Physical Systems, James Weimer, Radoslav Ivanov, Sanjian Chen, Alexander Roederer, Oleg Sokolsky, Insup Lee

#### Parameter-Invariant Monitor Design For Cyber Physical Systems, James Weimer, Radoslav Ivanov, Sanjian Chen, Alexander Roederer, Oleg Sokolsky, Insup Lee

*Departmental Papers (CIS)*

The tight interaction between information technology and the physical world inherent in Cyber-Physical Systems (CPS) can challenge traditional approaches for monitoring safety and security. Data collected for robust CPS monitoring is often sparse and may lack rich training data describing critical events/attacks. Moreover, CPS often operate in diverse environments that can have significant inter/intra-system variability. Furthermore, CPS monitors that are not robust to data sparsity and inter/intra-system variability may result in inconsistent performance and may not be trusted for monitoring safety and security. Towards overcoming these challenges, this paper presents recent work on the design of parameter-invariant ...

Smooth Operator: Control Using The Smooth Robustness Of Temporal Logic, Yash Vardhan Pant, Houssam Abbas, Rahul Mangharam

#### Smooth Operator: Control Using The Smooth Robustness Of Temporal Logic, Yash Vardhan Pant, Houssam Abbas, Rahul Mangharam

*Real-Time and Embedded Systems Lab (mLAB)*

Modern control systems, like controllers for swarms of quadrotors, must satisfy complex control objectives while withstanding a wide range of disturbances, from bugs in their software to attacks on their sensors and changes in their environments. These requirements go beyond stability and tracking, and involve temporal and sequencing constraints on system response to various events. This work formalizes the requirements as formulas in Metric Temporal Logic (MTL), and designs a controller that maximizes the robustness of the MTL formula. Formally, if the system satisfies the formula with robustness r, then any disturbance of size less than r cannot cause it ...

Resilient Linear Classification: An Approach To Deal With Attacks On Training Data, Sangdon Park, James Weimer, Insup Lee

#### Resilient Linear Classification: An Approach To Deal With Attacks On Training Data, Sangdon Park, James Weimer, Insup Lee

*Departmental Papers (CIS)*

Data-driven techniques are used in cyber-physical systems (CPS) for controlling autonomous vehicles, handling demand responses for energy management, and modeling human physiology for medical devices. These data-driven techniques extract models from training data, where their performance is often analyzed with respect to random errors in the training data. However, if the training data is maliciously altered by attackers, the effect of these attacks on the learning algorithms underpinning data-driven CPS have yet to be considered. In this paper, we analyze the resilience of classification algorithms to training data attacks. Specifically, a generic metric is proposed that is tailored to measure ...

Technical Report: Control Using The Smooth Robustness Of Temporal Logic, Yash Vardhan Pant, Houssam Abbas, Rahul Mangharam

#### Technical Report: Control Using The Smooth Robustness Of Temporal Logic, Yash Vardhan Pant, Houssam Abbas, Rahul Mangharam

*Real-Time and Embedded Systems Lab (mLAB)*

Cyber-Physical Systems must withstand a wide range of errors, from bugs in their software to attacks on their physical sensors. Given a formal specification of their desired behavior in Metric Temporal Logic (MTL), the robust semantics of the specification provides a notion of system robustness that can be calculated directly on the output behavior of the system, without explicit reference to the various sources or models of the errors. The robustness of the MTL specification has been used both to verify the system offline (via robustness minimization) and to control the system online (to maximize its robustness over some horizon ...

Relaxed Decidability And The Robust Semantics Of Metric Temporal Logic, Houssam Abbas, Matthew O'Kelly, Rahul Mangharam

#### Relaxed Decidability And The Robust Semantics Of Metric Temporal Logic, Houssam Abbas, Matthew O'Kelly, Rahul Mangharam

*Real-Time and Embedded Systems Lab (mLAB)*

Relaxed notions of decidability widen the scope of automatic verification of hybrid systems. In quasi-decidability and $\delta$-decidability, the fundamental compromise is that if we are willing to accept a slight error in the algorithm's answer, or a slight restriction on the class of problems we verify, then it is possible to obtain practically useful answers. This paper explores the connections between relaxed decidability and the robust semantics of Metric Temporal Logic formulas. It establishes a formal equivalence between the robustness degree of MTL specifications, and the imprecision parameter $\delta$ used in $\delta$-decidability when it is used to ...

Tech Report: Robust Model Predictive Control For Non-Linear Systems With Input And State Constraints Via Feedback Linearization, Yash Vardhan Pant, Houssam Abbas, Rahul Mangharam

#### Tech Report: Robust Model Predictive Control For Non-Linear Systems With Input And State Constraints Via Feedback Linearization, Yash Vardhan Pant, Houssam Abbas, Rahul Mangharam

*Real-Time and Embedded Systems Lab (mLAB)*

Robust predictive control of non-linear systems under state estimation errors and input and state constraints is a challenging problem, and solutions to it have generally involved solving computationally hard non-linear optimizations. Feedback linearization has reduced the computational burden, but has not yet been solved for robust model predictive control under estimation errors and constraints. In this paper, we solve this problem of robust control of a non-linear system under bounded state estimation errors and input and state constraints using feedback linearization. We do so by developing robust constraints on the feedback linearized system such that the non-linear system respects its ...

Robust Model Predictive Control For Non-Linear Systems With Input And State Constraints Via Feedback Linearization, Yash Vardhan Pant, Houssam Abbas, Rahul Mangharam

#### Robust Model Predictive Control For Non-Linear Systems With Input And State Constraints Via Feedback Linearization, Yash Vardhan Pant, Houssam Abbas, Rahul Mangharam

*Real-Time and Embedded Systems Lab (mLAB)*

Robust predictive control of non-linear systems under state estimation errors and input and state constraints is a challenging problem, and solutions to it have generally involved solving computationally hard non-linear optimizations. Feedback linearization has reduced the computational burden, but has not yet been solved for robust model predictive control under estimation errors and constraints. In this paper, we solve this problem of robust control of a non-linear system under bounded state estimation errors and input and state constraints using feedback linearization. We do so by developing robust constraints on the feedback linearized system such that the non-linear system respects its ...

Representation Of Confidence In Assurance Cases Using The Beta Distribution, Lian Duan, Sanjai Rayadurgam, Mats Heimdahl, Oleg Sokolsky, Insup Lee

#### Representation Of Confidence In Assurance Cases Using The Beta Distribution, Lian Duan, Sanjai Rayadurgam, Mats Heimdahl, Oleg Sokolsky, Insup Lee

*Departmental Papers (CIS)*

Assurance cases are used to document an argument that a system—such as a critical software system—satisfies some desirable property (e.g., safety, security, or reliability). Demonstrating high confidence that the claims made based on an assurance case can be trusted is crucial to the success of the case. Researchers have proposed quantification of confidence as a Baconian probability ratio of eliminated concerns about the assurance case to the total number of identified concerns. In this paper, we extend their work by mapping this discrete ratio to a continuous probability distribution—a beta distribution— enabling different visualizations of the ...

Co-Design Of Anytime Computation And Robust Control (Supplemental), Yash Vardhan Pant, Kartik Mohta, Houssam Abbas, Truong X Nghiem, Joesph Deveitti, Rahul Mangharam

#### Co-Design Of Anytime Computation And Robust Control (Supplemental), Yash Vardhan Pant, Kartik Mohta, Houssam Abbas, Truong X Nghiem, Joesph Deveitti, Rahul Mangharam

*Real-Time and Embedded Systems Lab (mLAB)*

No abstract provided.

Co-Design Of Anytime Computation And Robust Control, Yash Vardhan Pant, Kartik Mohta, Houssam Abbas, Truong Nghiem, Joesph Deveitti, Rahul Mangharam

#### Co-Design Of Anytime Computation And Robust Control, Yash Vardhan Pant, Kartik Mohta, Houssam Abbas, Truong Nghiem, Joesph Deveitti, Rahul Mangharam

*Real-Time and Embedded Systems Lab (mLAB)*

No abstract provided.

Requirement-Guided Model Refinement, Zhihao Jiang, Pieter Mosterman, Rahul Mangharam

#### Requirement-Guided Model Refinement, Zhihao Jiang, Pieter Mosterman, Rahul Mangharam

*Real-Time and Embedded Systems Lab (mLAB)*

Medical device is a typical Cyber-Physical System and ensuring the safety and efficacy of the device requires closed-loop verification. Currently closed-loop verifications of medical devices are performed in the form of clinical trials in which the devices are tested on the patients.

Expressiveness Of Streaming String Transducers, Rajeev Alur

#### Expressiveness Of Streaming String Transducers, Rajeev Alur

*Departmental Papers (CIS)*

Streaming string transducers define (partial) functions from input strings to output strings. A streaming string transducer makes a single pass through the input string and uses a finite set of variables that range over strings from the output alphabet. At every step, the transducer processes an input symbol, and updates all the variables in parallel using assignments whose right-hand-sides are concatenations of output symbols and variables with the restriction that a variable can be used at most once in a right-hand-side expression. It has been shown that streaming string transducers operating on strings over infinite data domains are of interest ...

On-The-Fly Reachability And Cycle Detection For Recursive State Machines, Rajeev Alur, Swarat Chaudhuri, Kousha Etessami, P. Madhusudan

#### On-The-Fly Reachability And Cycle Detection For Recursive State Machines, Rajeev Alur, Swarat Chaudhuri, Kousha Etessami, P. Madhusudan

*Departmental Papers (CIS)*

Searching the state space of a system using enumerative and on-the-fly depth-first traversal is an established technique for model checking finite-state systems. In this paper, we propose algorithms for on-the-fly exploration of recursive state machines, or equivalently pushdown systems, which are suited for modeling the behavior of procedural programs. We present algorithms for reachability (is a bad state reachable?) as well as for fair cycle detection (is there a reachable cycle with progress?). We also report on an implementation of these algorithms to check safety and liveness properties of recursive boolean programs, and its performance on existing benchmarks.