Our research focus is on development of high-assurance system design methodologies for Cyber-Physical Systems (CPS) with varying levels of autonomy and human interaction, which is at the confluence of AI, embedded systems, formal methods, controls and robotics. 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.

Active Projects

CAREER: Foundations for Secure Control of Cyber-Physical Systems (NSF CNS/CPS)Stealthy attacks on lane keeping

This project will develop scientific foundations for design of secure control of CPS, resulting in a high-assurance CPS design framework in which a mix of attack-resilient control, security-aware human-CPS interactions, and efficient controller instrumentation provides safety and performance guarantees even in the presence of attacks. Specifically, the goal of this project is to provide fundamentally new methods for security-aware modeling, analysis and design of safety-critical CPS, addressing the many different physical, functional and logical aspects of these heterogeneous systems in the presence of attacks. The proposed design framework will be used to develop security-aware automotive controllers for connected and autonomous vehicles with varying levels of autonomy and human supervision. More on security-aware CPS»

AFOSR Center of Excellence: Assuring Autonomy in Contested Environments (AFOSR CoE)

The University of Florida, Duke University, the University of Texas Austin, and the University of California Santa Cruz established an Air Force Office of Scientific Research (AFOSR) Center of Excellence (CoE) for Assured Autonomy in Contested Environments in collaboration with the Air Force Office of Scientific Research (AFOSR) and the munitions (RW), sensors (RY), and space vehicles (RV) directorates within the Air Force Research Laboratory (AFRL). Autonomous systems must execute high level missions plans with verifiable assurances despite uncertain adversarial environments where the integrity and availability of sensor information and communications are challenged. Key innovations include analysis, design and synthesis tools that enable autonomous mission execution despite uncertainty within complex dynamics while accounting for the integrity and privacy of information on computationally constrained resources. 

Platform-Level Services for Security of Naval Cyber-Physical Systems (ONR)

Details to come...

Security-Aware Human-on-the-Loop Cyber-Physical Systems

RESCHU-SACPSs 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


NSF IUCRC for Alternative Sustainable and Intelligent Computing (NSF IUCRC ASIC)

The NSF IUCRC for Alternative Sustainable and Intelligent Computing (ASIC) is a multi-site, multidisciplinary consortium that explores research frontiers in emerging computing platforms for cognitive applications. We are focused on four spheres of concentration: 1) Defense Technology, 2) Information Technology, 3) Infrastructure, and 4) Applications. The ASIC center focuses on designing alternative computing platforms for cognitive applications, whichperform inefficiently on conventional von Neumann architectures. The ASIC center is motivated by the recent rapid developments in technology related to cognitive applications. More»

Closed-loop STN/GPi Deep Brain Stimulation (NIH Brain Initiative)

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 learning-enables 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

Human-on-the-Loop Control for Smart Ultrasound Imaging (NSF CNS/CPS)

There can be large variability in medical image quality obtained by different experts imaging the same patient, which can affect successful diagnosis and patient treatment. This problem becomes even more pronounced across patients. Consequently, to decrease this variability this project will develop imaging techniques that are not passive but are based on real-time ultrasound beam control and adaptation, while facilitating best use of operator expertise to obtain the most informative images. Such new active ultrasound systems, where expert users with varying levels of training interact with a smart ultrasound device to improve medical imaging and facilitate diagnosis, will provide significant performance gains compared to present systems that are only manually controlled. This project will also have a significant societal impact in accurate, safe, and cost-effective diagnosis of many medical conditions, such as cancers or liver fibrosis.

Adaptive Protocol Synthesis and Error Recovery in Digital Microfluidic Biochips (NSF CCSS)

Droplet-based ("digital") microfluidic biochips (DMFBs) are revolutionizing high-throughput DNA sequencing and point-of-care clinical diagnosis. Micro-electrode-dot-array (MEDA) biochips have been recently developed, incorporating real-time capacitive sensing on every microelectrode to detect the property and location of a droplet. Such 'sensing maps' open up the exciting opportunity of cyber-physical MEDA biochips that can dynamically respond to bioassay outcomes, perform real-time error recovery, and execute "if-then-else" protocols from biochemistry necessary to support the next generation of cyber-physical systems (CPS) with tightly integrated lab-on-chip sensing technology. This research is motivated by the need to enable the execution of biomolecular assays on programmable and cyber-physical MEDA biochips. To take full advantage of the dynamic adaptation capabilities of MEDA, there is a need for a synthesis and run-time optimization framework that can be agile in its ability to respond to real-time sensor feedback. 


Past Projects

Design of High-Assurance Cyber-Physical Systems (ONR YIP)

The project aims to establish a high-assurance development framework for naval cyber-physical systems (CPS) that have to safely operate even in adversarial environments. Specifically, our goal is to ensure safe naval system operation and graceful performance degradation in contested environments. This will be accomplished by developing a set of design techniques and tools that: 1) incorporate security awareness into the design of cyber-physical components by exploiting the physical laws governing systems behavior, and 2) synthesize software tasks that correctly implement the developed cyber-physical components without introducing any security vulnerabilities. Development of the high-assurance design framework will be supplemented by a series of naval case studies, focused on design of modern vessels and unmanned aerial vehicles. These case studies with increasing scale and complexity will yield a comprehensive evaluation of the developed techniques and tools. More on security-aware CPS»

Security and Privacy-Aware Cyber-Physical Systems (Intel/NSF Partnership)

The project aims to achieve a comprehensive understanding of CPS-specific security and privacy challenges. This understanding will enable us to (1) develop techniques to prevent security attacks to CPS and to detect and recover from malicious attacks to CPS; (2) develop techniques for security-aware control design based on attack resilient state estimation; (3) ensure privacy of data collected and used by CPS, and (4) establish an evidence-based framework for CPS security and privacy assurance, taking into account the operating context of the system and human factors. Project webpage»   More on security-aware CPS»

Development of Control-Aware Cyber Techniques for Attack-Resilient Industrial Control & Combat Systems (ONR RHIMES)

The primary goal of the project is to develop techniques for ensuring that industrial control and combat systems (ICCS) are resilient to cyber-physical attacks; that is, attacks that combine conventional cyber intrusions with interference to the physical environment of ICCS. A number of such attacks have emerged recently. These incidents suggest that conventional information security approaches may not be effective in dealing with such attacks. This project will develop new security techniques specifically targeting cyber-physical attacks. The new techniques will be compatible with existing ICCS development techniques, allowing legacy ICCS to be retrofitted with enhanced security guarantees.

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. 

Design of Reconfigurable Manufacturing Systems

RMS animationModern 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. From Sequential Control Systems to Reconfigurable Machine Tools, RMS components must enable online system adaptation to facilitate manufacturing of diverse products through change of position and/or orientation of modules, modules swapping, and adding additional degrees of freedom and/or end effectors/spindles as needed. To achieve this, RMS necessitate the use of a dynamic controller architecture that is distributed, fully modular and self-configurable. Read more

Model-Based Design of Implantable Cardiac Devices

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.

Wireless Control Networks: A New Aprroach for Control over Networks

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»