Open Access. Powered by Scholars. Published by Universities.®

Engineering Commons

Open Access. Powered by Scholars. Published by Universities.®

Articles 1 - 22 of 22

Full-Text Articles in Engineering

Reconfiguring Non-Convex Holes In Pivoting Modular Cube Robots, Daniel Adam Feshbach, Cynthia Sung Jul 2021

Reconfiguring Non-Convex Holes In Pivoting Modular Cube Robots, Daniel Adam Feshbach, Cynthia Sung

Lab Papers (GRASP)

We present an algorithm for self-reconfiguration of admissible 3D configurations of pivoting modular cube robots with holes of arbitrary shape and number. Cube modules move across the surface of configurations by pivoting about shared edges, enabling configurations to reshape themselves. Previous work provides a reconfiguration algorithm for admissible 3D configurations containing no non-convex holes; we improve upon this by handling arbitrary admissible 3D configurations. The key insight specifies a point in the deconstruction of layers enclosing non-convex holes at which we can pause and move inner modules out of the hole. We prove this happens early enough to maintain connectivity ...


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

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 Apr 2019

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 Apr 2019

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 LITMUSRT 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 Apr 2018

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 Apr 2018

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 Apr 2018

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 Mar 2018

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 Feb 2018

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 Jan 2018

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 Aug 2017

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 Apr 2017

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 Mar 2017

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 Feb 2017

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 Mar 2016

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 Jan 2016

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 Jan 2016

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 May 2015

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 Jan 2015

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 Dec 2014

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 Jan 2010

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 Apr 2005

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.