|E-mail: miroslav.pajic AT duke.edu
E-mail: pajic AT seas.upenn.edu
Address: Room 203 Moore Building, 200 South 33rd Street, Philadelphia, PA 19104
My main research focus is on the control aspect of Cyber-Physical Systems (CPS), which is at the confluence of real-time embedded systems and control theory. The long-term goal is to build foundations for the composable modeling, design and analysis of these systems, while addressing issues such as safety, efficiency, robustness, and security. Since my research is frequently motivated by problems that occur during implementation and system integration, all my work involves system building and thorough experimental evaluation.
Along these lines my work has been focused on the following themes:
The current generations of embedded wireless networks address sensing and monitoring only and are largely open loop. To address actuation and closed-loop control, the communication architecture, protocols and interaction between communication and computation need to be re-thought. This will allow for the use the use of abstractions that effectively change the structure of the problem at hand. My goal is to develop a new class of wireless control networks where the automation systems are 'plug-n-play' - i.e. the wireless controller can be hot-swapped and the wireless I/O lines reconnect and maintain control performance and safety. This requires that the control functionality is decoupled from the inherently unreliable wireless substrate, and the control performance and stability is scalable with the number of nodes within the controller networks.
We introduce the concept of a Wireless Control Network (WCN) where the entire network itself acts as the controller - opposed to traditional networked control schemes where the nodes simply route information to and from a dedicated controller. Specifically, we formulate a simple, linear iterative strategy for each node in the network to follow, causing the entire network to behave as a linear dynamical system, with sparsity constraints imposed by the network topology. WCN introduces very low computational and communication overhead to the nodes in the network, allows for the use of simple transmission scheduling algorithms, and enables compositional design (where the existing wireless control infrastructure can be easily extended to handle new plants that are brought online in the vicinity of the network). More»
We have designed the Embedded Virtual Machine (EVM), a powerful and programmable runtime abstraction where a collection of physical nodes is composed into a single virtual controller. The virtual machine allows for migration of the controller tasks from one physical node to the most competent set of physical nodes, in the presence of node and link failures while maintaining the control law and timeliness requirements. EVM-based algorithms allow network control algorithms to operate seamlessly over less reliable wireless networks with topological changes. They introduce new capabilities such as predictable outcomes during sensor/actuator failure, adaptation to mode changes and runtime optimization of resource consumption. Furthermore, we utilize the EVM to develop a 3-layered design process to allow control engineers to design wireless control systems in a manner that is both largely platform/protocol/hardware/architecture independent and extensible to different domains of control systems (e.g., process control, aviation, medical). More»
The focus of the project is to devise a spatio-temporal jamming avoidance scheme for malicious jammers and unintentional interference in real-time wireless communication. In the context of energy-constrained embedded wireless networks, nodes are scheduled to maximize the common sleep duration and coordinate communication to extend their battery life. This coordination results in statistical and predictable activity patterns that may be easily detected and jammed. The key idea is to remove any spatio-temporal patterns of channel activities while ensuring coordinated and collision-free operation. WisperNet employs hardware-based time synchronization and lightweight cryptographic hashing for coordinated temporal randomization of slot schedules (at the link layer) and adapts routes to avoid static jammers (in the network layer). More»
I have been pursuing a parallel research track on Medical Cyber-Physical Systems (MCPSs) with so-called "messy plants", such as the human body or heart. Software failures resulted in 24% of all medical device recalls in 2011, while almost 2,000,000 software-based devices have been recalled in the past decade. Surprisingly, given the situation, there is no formal design methodology or open experimental platforms that can be used to ensure the correct operation of medical devices within the physiological closed-loop context. This effectively prevents software-controlled medical devices in reaching the full potential in providing the best possible patient care, while significantly reducing the soaring healthcare costs. To this effect, my work in this theme has been focused on the development of high-confidence medical systems where a single device or several interoperable devices are used for physiological closed-loop control.
To improve patient safety and healthcare efficiency, in modern hospitals patients are treated using a wide array of medical devices that are increasingly interacting over the network. However, to reduce the burden on caregivers and the overall health-care costs, it is necessary to guarantee safety and effectiveness of interoperating medical devices.
The main challenges in these closed-loop scenarios are insufficient understanding of the human body's response to treatment, and the high degree of parametric uncertainty and variability between patients.
To study effects of the medical device interconnectivity and interoperability with network-enabled control on the patient safety, we have considered a closed-loop clinical scenario: a system for the physiologic closed-loop control of drug infusion. The main contribution of our work is the verification approach for the safety properties of closed-loop medical systems. Our method combines robust-control techniques and simulation-based analysis of a detailed model of the system (including continuous-time patient dynamics with uncertain parameters) with model checking of a more abstract timed-automata model. We have shown that the relationship between the two models preserves the crucial aspect of the timing behavior, thus, ensuring the conservativeness of the safety analysis. We also describe a system design that can guarantee open-loop safety under network failure. [TII'13], [ICCPS'10]
Safety recalls of pacemakers and implantable cardioverter defibrillators due to firmware problems affected over 200,000 devices between 1990 and 2000, comprising 41% of the devices recalled.
Despite increasing complexity of cardiac pacemakers, the only method currently used to check for correctness of the device operation is unit testing based on a playback of pre-recorded electrogram signals. This open-loop "tape" testing is unable to check for safety violations due to inappropriate stimulus by the pacemaker, highlighting the need for interactive closed-loop verification and testing of such systems. We have created a model-driven development framework for safety-critical implantable cardiac devices that includes integrates system modeling, verification, model-based WCET analysis, simulation, modular code generation, and testing. To enable the framework, I have developed the UPP2SF tool for automatic translation of verified models (in UPPAAL) to models that may be simulated and tested (in Simulink). The translation guarantees that verified abstract models over-approximate the detailed models used downstream for simulation and code generation, thus ensuring that the closed-loop safety properties are retained through the tool-chain.
Real-time Virtual Heart Model (VHM) models the electrophysiological operation of the functioning (i.e. during normal sinus rhythm) and malfunctioning (i.e. during arrhythmia) heart. 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. More»
Modern embedded control architectures have moved from isolated closed-loop control systems to open architectures, such as new automotive architectures with services that include remote diagnostics, code updates, and vehicle-to-vehicle communication. However, this shift has also introduced security vulnerabilities that are easily exploitable, since the current embedded systems have not been built with security in mind. An illustrative example are the recently exposed security vulnerabilities in present-day vehicles, which can be simply exploited by an attacker to disrupt the operation of a car by either disabling the vehicle or hijack it, giving the attacker the ability to control it instead. The challenge of designing secure embedded-control systems has to be addressed on two levels. First, it is necessary to design attack resilient control schemes and architectures, capable of dealing with attacks on the environment of the controller, including attacks on sensors, actuators, and communication media. To utilize the knowledge of the system dynamics for attack detection and identification, we have to focus on new problems, such as sensor and controller fusion under attacks, detecting system attacks in the presence of noise and model uncertainty, and resilient control of nonlinear systems. On the other level, it is essential to ensure that the code generated for the resilient controller correctly implements the desired algorithm while preventing injection of malicious code into the controller itself. This can be achieved by providing a set of control and security code invariants that can be verified under a certain set of assumptions on the underlying computation/communication platform. In this case, the main challenges are in defining a suitable set of control invariants, along with formalisms that can be used to capture the platform assumptions. More»