Mangharam, Rahul
Email Address
ORCID
Disciplines
relationships.isProjectOf
relationships.isOrgUnitOf
Position
Faculty Member
Introduction
Rahul's focus is on the development of life-critical and safety-critical real-time embedded systems in medical devices, automotive electronics, wireless control networks and energy-efficient buildings. He directs mLAB::Real-Time and Embedded Systems Lab, which develops software verification and testing techniques for high-confidence medical devices such as implantable cardiac pacemakers; new designs for automotive electronic controllers to develop programmable vehicles of the future; distributed wireless control networks for closed-loop industrial automation, and new scheduling/control algorithms for energy-efficient buildings.
Research Interests
Collection
115 results
Search Results
Now showing 1 - 10 of 115
Publication Technical Report: Abstraction-Tree For Closed-loop Model Checking of Medical Devices(2015-05-06) Jiang, Zhihao; Abbas, Houssam; Mosterman, Pieter J; Mangharam, RahulPublication Topological conditions for in-network stabilization of dynamical systems(2013-04-01) Pajic, Miroslav; Sundaram, Shreyas; Mangharam, Rahul; Pappas, GeorgeWe study the problem of stabilizing a linear system over a wireless network using a simple in-network computation method. Specifically, we study an architecture called the "Wireless Control Network'' (WCN), where each wireless node maintains a state, and periodically updates it as a linear combination of neighboring plant outputs and node states. This architecture has previously been shown to have low computational overhead and beneficial scheduling and compositionality properties. In this paper we characterize fundamental topological conditions to allow stabilization using such a scheme. To achieve this, we exploit the fact that the WCN scheme causes the network to act as a linear dynamical system, and analyze the coupling between the plant's dynamics and the dynamics of the network. We show that stabilizing control inputs can be computed in-network if the vertex connectivity of the network is larger than the geometric multiplicity of any unstable eigenvalue of the plant. This condition is analogous to the typical min-cut condition required in classical information dissemination problems. Furthermore, we specify equivalent topological conditions for stabilization over a wired (or point-to-point) network that employs network coding in a traditional way -- as a communication mechanism between the plant's sensors and decentralized controllers at the actuators.Publication Scalable Scheduling of Building Control Systems for Peak Demand Reduction(2012-06-15) Nghiem, Truong; Behl, Madhur; Mangharam, Rahul; Pappas, GeorgeIn large energy systems, peak demand might cause severe issues such as service disruption and high cost of energy production and distribution. Under the widely adopted peak-demand pricing policy, electricity customers are charged a very high price for their maximum demand to discourage their energy usage in peak load conditions. In buildings, peak demand is often the result of temporally correlated energy demand surges caused by uncoordinated operation of sub-systems such as heating, ventilating, air conditioning and refrigeration (HVAC&R) systems and lighting systems. We have previously presented green scheduling as an approach to schedule the building control systems within a constrained peak demand envelope while ensuring that custom climate conditions are facilitated. This paper provides a sufficient schedulability condition for the peak constraint to be realizable for a large and practical class of system dynamics that can capture certain nonlinear dynamics, inter-dependencies, and constrained disturbances. We also present a method for synthesizing periodic schedules for the system. The proposed method is demonstrated in a simulation example to be scalable and effective for a large-scale system.Publication Evaluation of DR-Advisor on the ASHRAE Great Energy Predictor Shootout Challenge(2014-07-24) Behl, Madhur; Mangharam, RahulThis paper describes the evaluation of DR-Advisor algorithms on ''The Great Energy Predictor Shootout - The First Building Data Analysis and Prediction Competition'' held in 1993-94 by ASHRAE.Publication Towards Synthesis of Platform-Aware Attack-Resilient Control Systems: Extended Abstract(2013-04-09) Pajic, Miroslav; Bezzo, Nicola; Weimer, James; Alur, Rajeev; Mangharam, Rahul; Michael, Nathan; Pappas, George J; Sokolsky, Oleg; Tabuada, Paulo; Weirich, Stephanie; Lee, InsupPublication Real-time Heart Model for Implantable Cardiac Device Validation and Verification(2010-01-20) Jiang, Zhihao; Pajic, Miroslav; Connolly, Allison T; Dixit, Sanjay; Mangharam, RahulDesigning bug-free medical device software is dif- ficult, especially in complex implantable devices that may be used in unanticipated contexts. Safety recalls of pacemakers and implantable cardioverter defibrillators due to firmware problems between 1990 and 2000 affected over 200,000 devices, comprising 41% of the devices recalled and are increasing in frequency. There is currently no formal methodology or open experimental platform to validate and verify the correct operation of medical device software. To this effect, a real-time Virtual Heart Model (VHM) has been developed to model the electrophysiological operation of the functioning (i.e. during normal sinus rhythm) and malfunctioning (i.e. during arrhythmia) heart. We present a methodology to extract timing properties of the heart to construct a timed-automata model. The platform exposes functional and formal interfaces for validation and verification of implantable cardiac devices. We demonstrate the VHM is capable of generating clinically-relevant response to intrinsic (i.e. premature stimuli) and external (i.e. artificial pacemaker) signals for a variety of common arrhythmias. By connecting the VHM with a pacemaker model, we are able to pace and synchronize the heart during the onset of irregular heart rhythms. The VHM has also been implemented on a hardware platform for closed-loop experimentation with existing and virtual medical devices. The VHM allows for exploratory electrophysiology studies for physicians to evaluate their diagnosis and determine the appropriate device therapy. This integrated functional and formal device design approach will potentially help expedite medical device certification for safer operation.Publication Computer Aided Clinical Trials for Implantable Cardiac Devices(2016-08-19) Abbas, Houssam; Jiang, Zhihao; Jang, Kuk Jin; Beccani, Marco; Liang, Jackson; Dixit, Sanjay; Mangharam, RahulIn this effort we investigate the design and use of physiological and device models to conduct pre-clinical trials to provide early insight in the design and execution of the actual clinical trial. Computer models of physiological phenomena like cardiac electrical activity can be extremely complex. However, when the purpose of the model is to interact with a medical device, then it becomes sufficient to model the measurements that the device makes, e.g. the intra-cardiac electrograms (EGMs) that an Implantable Cardioverter Defibrillator (ICD) measures. We present a probabilistic generative model of EGMs, capable of generating exemplars of various arrhythmias. The model uses deformable shape templates, or motifs, to capture the variability in EGM shapes within one EGM channel, and a cycle length parameter to capture the variability in cycle length in one EGM channel. The relation between EGM channels, which is essential for determining whether the current arrhythmia is potentially fatal, is captured by a time-delayed Markov chain, whose states model the various combinations of (learned) motifs. The heart model is minimally parameterized and is learned from real patient data. Thus the statistics of key features reflect the statistics of a real cohort, but the model can also generate rare cases and new combinations from the inferred probabilities. On the device end, algorithms for signal sensing, detection and discrimination for major ICD manufacturers have been implemented both in simulation and on hardware platforms. The generated arrhythmia episodes are used as input to both the modeled ICD algorithms and real ICDs as part of a Computer Aided Clinical Trial (CACT). In a CACT, a computer model simulates the inputs to the device (such as a new, investigational ICD), and the device’s performance is evaluated. By incorporating these results into the appropriate statistical framework, the Computer Aided Clinical Trial results can serve as regulatory evidence when planning and executing an actual clinical trial. We demonstrate this by conducting a mock trial similar to the 2005-2010 RIGHT trial which compared the discrimination algorithms from two major ICD manufacturers. The results of the CACT clearly demonstrate that the failed outcome of the RIGHT trial could have been predicted and provides statistical support for deeper results that could have been captured prior to the trial.Publication A Simple Distributed Method for Control over Wireless Networks(2011-04-01) Pajic, Miroslav; Sundaram, Shreyas; Pappas, George; Mangharam, RahulWe present a distributed scheme used for control over wireless networks. In our previous work, we introduced the concept of a Wireless Control Network (WCN), where the network itself, with no centralized node, acts as the controller. In this work, we show how the WCN can be modified to include observer style updates which substantially improves robustness of the closed-loop system to link failures. In addition, we analyze how the WCN simplifies extraction of the communication and computation schedules and enables system compositionality and scalability.Publication RT-Link: A Time-Synchronized Link Protocol for Energy-Constrained Multi-hop Wireless Networks(2006-09-01) Mangharam, Rahul; Rowe, Anthoney; Rajkumar, RajWe propose RT-Link, a time-synchronized link protocol for real-time wireless communication in industrial control, surveillance and inventory tracking. RT-Link provides predictable lifetime for battery-operated embedded nodes, bounded end-to-end delay across multiple hops, and collision-free operation. We investigate the use of hardwarebased time-synchronization for infrastructure nodes by using an AM carrier-current radio for indoors and atomic clock receivers for outdoors. Mobile nodes are synchronized via in-band software synchronization within the same framework. We identify three key observations in the design and deployment of RT-Link: (a) Hardware-based global-time synchronization is a robust and scalable option to in-band softwarebased techniques. (b) Achieving global time-synchronization is both economical and convenient for indoor and outdoor deployments. (c) RT-Link achieves a practical lifetime of over 2 years. Through analysis and simulation, we show that RTLink outperforms energy-efficient link protocols such as BMAC in terms of node lifetime and end-to-end latency. The protocol supports flexible services such as on-demand endto- end rate control and logical topology control. We implemented RT-Link on the CMU FireFly sensor platform and have integrated it within the nano-RK real-time sensor OS. A 42-node network with sub-20us synchronization accuracy has been deployed for 3 weeks in the NIOSH Mining Research Laboratory and within two 5-story campus buildings.Publication Uncertainty Propagation from Sensing to Modeling and Control in Buildings - Technical Report(2013-10-19) Behl, Madhur; Nghiem, Truong; Mangharam, RahulA fundamental problem in the design of closed-loop Cyber-Physical Systems (CPS) is in accurately capturing the dynamics of the underlying physical system. To provide optimal control for such closed-loop systems, model-based controls require accurate physical plant models. It is hard to analytically establish (a) how data quality from sensors affects model accuracy, and consequently, (b) the effect of model accuracy on the operational cost of model-based controllers. We present the Model-IQ toolbox which, given a plant model and real input data, automatically evaluates the effect of this uncertainty propagation from sensor data to model accuracy to controller performance. We apply the Model-IQ uncertainty analysis for model-based controls in buildings to demonstrate the cost-benefit of adding temporary sensors to capture a building model. Model-IQ's automated process lowers the cost of sensor deployment, model training and evaluation of advanced controls for small and medium sized buildings. Model-IQ provides recommendation of sensor placement and density to trade-off the cost of additional sensors with energy savings by the improved controller performance. Such end-to-end analysis of uncertainty propagation has the potential to lower the cost for CPS with closed-loop model based control. We demonstrate this with real building data in the Department of Energy's HUB.