Our research focus is on development of high-assurance system design methodologies for Cyber-Physical Systems (CPS), which is at the confluence of embedded systems, formal methods and control theory. The long-term goal is to integrate system modeling, analysis and automatic synthesis into composable design procedures that ensure closed-loop system safety and desired performance under known and unknown operating conditions, and even in the presence of malicious activity.
Since our research is frequently motivated by problems that occur during implementation and system integration, all our work involves system building and thorough experimental evaluation.
CAREER: Foundations for Secure Control of Cyber-Physical Systems (NSF CNS/CPS)
Details to come...
Design of High-Assurance Cyber-Physical Systems (ONR YIP)
Details to come...
Development of Control-Aware Cyber Techniques for Attack-Resilient Industrial Control & Combat Systems (ONR RHIMES)
Details to come...
Security and Privacy-Aware Cyber-Physical Systems (Intel/NSF Partnership)
Details to come...
CPSs usually involve humans to aid with situations of higher degrees of uncertainty. In CPSL, we explore the impact of this human-autonomy interaction on the security of Unmanned Vehicles (UVs) supervisory systems, typically prone to cyber attacks on navigational sensors. Can we exploit this understanding and synthesis collaborative protocols for both the human operator and UVs towards higher security guarantees? Read more
Parkinson’s disease (PD) is the second most prevalent neurological disorder, affecting nearly one million people in the US, with 60,000 new cases diagnosed every year. Deep Brain Stimulation (DBS) is effective at alleviating symptoms of PD and several other neurological disorders. Yet, despite its safety-critical nature, there does not exist a platform for integrated design and testing of DBS devices.
We intend to fill this gap, and provide a platform that implements an accurate physiological simulation of the region of the brain that is believed to be the source of the disease and a target of DBS devices, known as Basal Ganglia (BG), in real time. Thus, this platform's intended use is the test of existing DBS controllers, and the design of the novel ones. Currently, we are working on further improvements of the platform mainly related to the relevant neural data analysis on-the-fly, design of optimal DBS controllers, and acceleration of the controller design. Read more
Adaptive Protocol Synthesis and Error Recovery in Digital Microfluidic Biochips
Details to come...
Design of Reconfigurable Manufacturing Systems
Modern manufacturing systems require fast and effective adaptation to fluctuating market conditions and product diversification. This high level of adaptability can be achieved through the use of Reconfigurable Manufacturing Systems (RMS), which should be based on modular equipment that is easily integrated, scalable, convertible in terms of functionality, and self-diagnosable. Major components of RMS are Reconfigurable Machine Tools that enable online system adaptation to facilitate manufacturing of diverse products through change of position and/or orientation of modules, modules swapping, and adding additional axes and/or spindles as needed. To achieve this, RMS necessitate the use of a dynamic controller architecture that is distributed, fully modular and self-configurable.
We illustrate the use of our design framework for reconfigurable machine tools through design of modularized and distributed Computer Numerical Control (CNC). Specifically, we focus on design challenges for Plug-n-Play automation systems, where new system functionalities, such as adding new degrees of freedom (axes) in existing CNC units, can be introduced without significant reconfiguration efforts and downtime costs. We propose a fully distributed motion control architecture realized through a network of individual axis control modules. Reconfiguration of motion control systems based on this architecture can be achieved by only presenting the controller on each axis with information about machine configuration and the type of axis. This effectively enables modularity, reconfigurability, and interoperability of the machine control system.
Design of High-Assurance Autonomous Vehicles (DARPA High-Assurance Cyber Military Systems (HAMCS) Program)
The focus of the project work is twofold. We provide algorithms with quantifiable guarantees for attack-resilient control of autonomous ground vehicles, such as the Landshark and American Built Car (ABC), and unmanned aerial vehicles (e.g., 3DR Quadcopter). To achieve this, we consider attack scenarios where vehicles sensors and actuators are compromised and used by a malicious attacker to insert signals into the control loop. Furthermore, we will derive procedures that can be used to obtain worst-case performance guarantees for the control systems under attack. The second focus of our work is on creating design methods that result in high-assurance guarantees for control software used to implement the aforementioned algorithms. By starting from the control algorithms’ specification and requirements, we plan to define sets of invariants and illustrate its use for verification of control code implemented in C; the initial verification framework we plan to develop will be based on a Frama-C/Why3/Z3 toolchain.
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. More»
Real-Time Virtual Heart Model
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.
We introduce the concept of a Wireless Control Network (WCN) where the entire network itself acts as the controller, unlike 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»