Open Access. Powered by Scholars. Published by Universities.®
- Discipline
- Keyword
-
- Real-time systems (4)
- Cyber-Physical Systems (3)
- Embedded systems (3)
- Fault-tolerant systems (3)
- Protocols (3)
-
- Security (3)
- Telecommunication network reliability (3)
- Wireless networks (3)
- Wireless sensor networks (3)
- Anti jamming protocol (2)
- Anti-jamming (2)
- Battery life maximization (2)
- Censorship-to-link utilization ratio (2)
- Communication protocol (2)
- Contention-free communication (2)
- Coordinated temporal randomization (2)
- Electromagnetic jamming (2)
- Embedded wireless network (2)
- Energy-constrained wireless sensor network (2)
- Jamming (2)
- Link layer slot duration (2)
- Link layer slot schedule (2)
- MAC protocol (2)
- Malicious jamming (2)
- Medical devices (2)
- Network Control Systems (2)
- Node scheduling (2)
- Random jammer (2)
- Random processes (2)
- Spatio-temporal pattern (2)
- File Type
Articles 1 - 12 of 12
Full-Text Articles in Computer Engineering
Wispernet: Anti-Jamming For Wireless Sensor Networks, Miroslav Pajic, Rahul Mangharam
Wispernet: Anti-Jamming For Wireless Sensor Networks, Miroslav Pajic, Rahul Mangharam
Rahul Mangharam
Resilience to electromagnetic jamming and its avoidance are difficult problems. It is often both hard to distinguish malicious jamming from congestion in the broadcast regime and a challenge to conceal the activity patterns of the legitimate communication protocol from the jammer. In the context of energy-constrained wireless sensor networks, nodes are scheduled to maximize the common sleep duration and coordinate communication to extend their battery life. This results in well-defined communication patterns with possibly predictable intervals of activity that are easily detected and jammed by a statistical jammer. We present an anti-jamming protocol for sensor networks which eliminates spatio-temporal patterns …
Modeling And Verification Of A Dual Chamber Implantable Pacemaker, Zhihao Jiang, Miroslav Pajic, Salar Moarref, Rajeev Alur, Rahul Mangharam
Modeling And Verification Of A Dual Chamber Implantable Pacemaker, Zhihao Jiang, Miroslav Pajic, Salar Moarref, Rajeev Alur, Rahul Mangharam
Rahul Mangharam
The design and implementation of software for medical devices is challenging due to their rapidly increasing functionality and the tight coupling of computation, control, and communication. The safety-critical nature and the lack of existing industry standards for verification, make this an ideal domain for exploring applications of formal modeling and analysis. In this study, we use a dual chamber implantable pacemaker as a case study for modeling and verification of control algorithms for medical devices in UPPAAL. We begin with detailed models of the pacemaker, based on the specifications and algorithm descriptions from Boston Scientific. We then define the state …
Cyber-Physical Modeling Of Implantable Cardiac Medical Devices, Zhihao Jiang, Miroslav Pajic, Rahul Mangharam
Cyber-Physical Modeling Of Implantable Cardiac Medical Devices, Zhihao Jiang, Miroslav Pajic, Rahul Mangharam
Rahul Mangharam
The design of bug-free and safe medical device software is challenging, especially in complex implantable devices that control and actuate organs in unanticipated contexts. Safety recalls of pacemakers and implantable cardioverter defibrillators between 1990 and 2000 affected over 600,000 devices. Of these, 200,000 or 41%, were due to firmware issues and their effect continues to increase in frequency. There is currently no formal methodology or open experimental platform to test and verify the correct operation of medical device software within the closed-loop context of the patient. To this effect, a real-time Virtual Heart Model (VHM) has been developed to model …
From Verification To Implementation: A Model Translation Tool And A Pacemaker Case Study, Miroslav Pajic, Zhihao Jiang, Insup Lee, Oleg Sokolsky, Rahul Mangharam
From Verification To Implementation: A Model Translation Tool And A Pacemaker Case Study, Miroslav Pajic, Zhihao Jiang, Insup Lee, Oleg Sokolsky, Rahul Mangharam
Rahul Mangharam
Model-Driven Design (MDD) of cyber-physical systems advocates for design procedures that start with formal modeling of the real-time system, followed by the model’s verification at an early stage. The verified model must then be translated to a more detailed model for simulation-based testing and finally translated into executable code in a physical implementation. As later stages build on the same core model, it is essential that models used earlier in the pipeline are valid approximations of the more detailed models developed downstream. The focus of this effort is on the design and development of a model translation tool, UPP2SF, and …
The Wireless Control Network: Synthesis And Robustness, Miroslav Pajic, Shreyas Sundaram, Jerome Le Ny, George J. Pappas, Rahul Mangharam
The Wireless Control Network: Synthesis And Robustness, Miroslav Pajic, Shreyas Sundaram, Jerome Le Ny, George J. Pappas, Rahul Mangharam
Rahul Mangharam
We consider the problem of stabilizing a plant with a network of resource constrained wireless nodes. Traditional networked control schemes are designed with one of the nodes in the network acting as a dedicated controller, while the other nodes simply route information to and from the controller and the plant. We introduce the concept of a Wireless Control Network (WCN) where the entire network itself acts as the controller. Specifically, at each time-step, each node updates its internal state to be a linear combination of the states of the nodes in its neighborhood. We show that this causes the entire …
Anti-Jamming For Embedded Wireless Networks, Miroslav Pajic, Rahul Mangharam
Anti-Jamming For Embedded Wireless Networks, Miroslav Pajic, Rahul Mangharam
Rahul Mangharam
Resilience to electromagnetic jamming and its avoidance are difficult problems. It is often both hard to distinguish malicious jamming from congestion in the broadcast regime and a challenge to conceal the activity patterns of the legitimate communication protocol from the jammer. In the context of energy-constrained wireless sensor networks, nodes are scheduled to maximize the common sleep duration and coordinate communication to extend their battery life. This results in well-defined communication patterns with possibly predictable intervals of activity that are easily detected and jammed by a statistical jammer. We present an anti-jamming protocol for sensor networks which eliminates spatio-temporal patterns …
Embedded Virtual Machines For Robust Wireless Control Systems, Rahul Mangharam, Miroslav Pajic
Embedded Virtual Machines For Robust Wireless Control Systems, Rahul Mangharam, Miroslav Pajic
Rahul Mangharam
Embedded wireless networks have largely focused on open loop sensing and monitoring. To address actuation in closed loop wireless control systems there is a strong need to re-think the communication architectures and protocols for reliability, coordination and control. As the links, nodes and topology of wireless systems are inherently unreliable, such time-critical and safety-critical applications require programming abstractions where the tasks are assigned to the sensors, actuators and controllers as a single component rather than statically mapping a set of tasks to a specific physical node at design time. To this end, we introduce the Embedded Virtual Machine (EVM), a …
Using The Virtual Heart Model To Validate The Mode-Switch Pacemaker Operation, Zhihao Jiang, Allison Connolly, Rahul Mangharam
Using The Virtual Heart Model To Validate The Mode-Switch Pacemaker Operation, Zhihao Jiang, Allison Connolly, Rahul Mangharam
Rahul Mangharam
Artificial pacemakers are one of the most widely-used implantable devices today, with millions implanted worldwide. The main purpose of an artificial pacemaker is to treat bradycardia, or slow heart beats, by pacing the atrium and ventricles at a faster rate. While the basic functionality of the device is fairly simple, there are many documented cases of death and injury due to device malfunctions. The frequency of malfunctions due to firmware problems will only increase as the pacemaker operations become more complex in an attempt to expand the use of the device. One reason these malfunctions arise is that there is …
The Wireless Control Network: Monitoring For Malicious Behavior, Shreyas Sundaram, Miroslav Pajic, Christoforos Hadjicostis, Rahul Mangharam, George Pappas
The Wireless Control Network: Monitoring For Malicious Behavior, Shreyas Sundaram, Miroslav Pajic, Christoforos Hadjicostis, Rahul Mangharam, George Pappas
Rahul Mangharam
We consider the problem of stabilizing a plant with a network of resource constrained wireless nodes. In a companion paper, we developed a protocol where each node repeatedly transmits a linear combination of the values in its neighborhood. For certain topologies, we showed that these linear combinations can be designed so that the closed loop system is stable (i.e., the wireless network itself acts as a controller for the plant). In this paper, we design a Intrusion Detection System (IDS) for this control scheme, which observes the transmissions of certain nodes in the network and uses that information to (a) …
Modeling Cardiac Pacemaker Malfunctions With The Virtual Heart Model, Zhihao Jiang, Rahul Mangharam
Modeling Cardiac Pacemaker Malfunctions With The Virtual Heart Model, Zhihao Jiang, Rahul Mangharam
Rahul Mangharam
Implantable cardiac devices such as artificial pacemakers deliver therapies according to the timing information from the heart. Such devices work under the assumptions of perfect sensing, which are: (a) the pacemaker leads remain in place, and (b) the pacing therapy in one chamber (e.g. atrium) is insulated from the other chambers (e.g. ventricles). But there are common cases which violate these assumptions and the mechanisms for imperfect sensing cannot be captured by a simple signal generator. In this paper we use the Penn Virtual Heart Model (VHM) to investigate the spatial and temporal aspects of the electrical conduction system of …
Embedded Virtual Machines For Robust Wireless Control And Actuation, Miroslav Pajic, Rahul Mangharam
Embedded Virtual Machines For Robust Wireless Control And Actuation, Miroslav Pajic, Rahul Mangharam
Rahul Mangharam
Embedded wireless networks have largely focused on open-loop sensing and monitoring. To address actuation in closed-loop wireless control systems there is a strong need to re-think the communication architectures and protocols for reliability, coordination and control. As the links, nodes and topology of wireless systems are inherently unreliable, such time-critical and safety-critical applications require programming abstractions and runtime systems where the tasks are assigned to the sensors, actuators and controllers as a single component rather than statically mapping a set of tasks to a specific physical node at design time. To this end, we introduce the Embedded Virtual Machine (EVM), …
Model-Based Closed-Loop Testing Of Implantable Pacemakers, Zhihao Jiang, Miroslav Pajic, Rahul Mangharam
Model-Based Closed-Loop Testing Of Implantable Pacemakers, Zhihao Jiang, Miroslav Pajic, Rahul Mangharam
Rahul Mangharam
The increasing complexity of software in implantable medical devices such as cardiac pacemakers and defibrillators accounts for over 40% of device recalls. Testing remains the principal means of verification in the medical device certification regime. Traditional software test generation techniques, where the tests are generated independently of the operational environment, are not effective as the device must be tested within the context of the patient's condition and the current state of the heart. It is necessary for the testing system to observe the system state and conditionally generate the next input to advance the purpose of the test. To this …