Computer systems are increasingly coming to be relied upon to augment or replace human operators in controlling mechanical devices in contexts such as transportation systems, chemical plants, and medical devices, where safety and correctness are critical. A central problem is how to verify that such partially automated or fully autonomous cyber-physical systems (CPS) are worthy of our trust. One promising approach involves synthesis of the computer implementation codes from formal specifications, by software tools. This project contributes to this "correct-by-construction" approach, by developing scalable, automated methods for the synthesis of control protocols with provable correctness guarantees, based on insights from models of human behavior. It targets: (i) the gap between the capabilities of today's hardly autonomous, unmanned systems and the levels of capability at which they can make an impact on our use of monetary, labor, and time resources; and (ii) the lack of computational, automated, scalable tools suitable for the specification, synthesis and verification of such autonomous systems. The research is based on study of modular reinforcement learning-based models of human behavior derived through experiments designed to elicit information on how humans control complex interactive systems in dynamic environments, including automobile driving. Architectural insights and stochastic models from this study are incorporated with a specification language based on linear temporal logic, to guide the synthesis of adaptive autonomous controllers. Motion planning and other dynamic decision-making are by algorithms based on computational engines that represent the underlying physics, with provision for run-time adaptation to account for changing operational and environmental conditions. Tools implementing this methodology are validated through experimentation in a virtual testing facility in the context of autonomous driving in urban environments and multi-vehicle autonomous navigation of micro-air vehicles in dynamic environments. Education and outreach activities include involvement of undergraduate and graduate students in the research, integration of the research into courses, demonstrations for K-12 students, and recruitment of research participants from under-represented demographic groups. Data, code, and teaching materials developed by the project are disseminated publicly on the Web.

This project develops a novel Cyber Physical System (CPS) centric approach to privacy and security for wireless networked CPS systems, by reconciling the low-delay and low-jitter requirements of CPS applications with the requirements imposed by security and privacy. Our starting observation is that, in CPS, an adversary's primary goal is not to learn all the raw data, but instead core attributes, such as the state or control actions that are derived from data. Building on this observation, we propose to use a distortion measure for security that maximizes the difference between the eavesdropper's estimate and the true value of the function computing the attributes of interest, reducing the adversary's ability to disrupt normal operation of CPS. We posit that we can protect these core attributes with fewer resources than needed to protect all the raw data. Ensuring secure and private information exchange over networked CPS systems is essential to building a thriving ecosystem of applications that range from autonomous cars and drones, to the Internet-of-Things (IoT), to immersive environments such as augmented reality for health, education, and collaboration. Our educational plan engages not only graduate students and postdocs but also high school and undergraduate students. It also reaches out to engineers and the lay public, by providing open source implementations of our algorithms making them available both to industry and hobbyists. The project considers both passive and active attacks. We will quantify novel privacy and security measures for CPS systems that are based on distortion measurements in a metric space; we will develop fundamental bounds as well as low complexity and low overhead coding schemes; we will quantify the disruptive power of active adversaries and design pro-active and retro-active defense mechanisms; and we will illustrate our approach over a flagship application, drone localization. Our approach will offer an alternative to wireless network encryption methods, by designing for low-delay, low-jitter requirements of CPS.

Modern electric power grid is a complex, interconnected cyber physical system (CPS) that forms the lifeline of our society. Reliable, secure, and efficient operation of the grid are of paramount importance to national security and economic well-being. Recent trends in security indicate the increasing threat of cyber-based attacks, both in numbers and sophistication, on energy and other critical infrastructure systems of our nation and the world in general. To address this growing threat, there is a compelling research need to develop a holistic cyber security framework that encompasses attack deterrence, attack prevention, attack detection, attack mitigation and resilience, and attack attribution and forensics. Risk assessment is one of the fundamental building blocks that cut across attack prevention, mitigation, and resilience. The existing tools for risk assessment and mitigation are mostly qualitative and often subjective, and hence they are grossly inadequate to capture the dynamic and uncertain nature of the adversaries and the complex cyber-physical couplings that exist in the grid. This project will develop a scientific methodology, algorithms, and tools for cyber risk assessment, attack-defense modeling, and cyber contingency analysis by leveraging game theoretic tools and solution strategies. The developed security algorithms and tools will be evaluated in a realistic CPS security testbed environment at Iowa State University and the results will be broadly shared with research community and also with industry for potential adoption. The innovative applications of game theoretic formulations and tools will help to develop secure and resilient algorithms that will prevent and mitigate attacks and will make the future grid resilient to both faults and cyber-attacks. The research also will have broader impacts in improving the security and resiliency of other CPS-based critical infrastructure systems, such as oil and natural gas networks and transportation networks. Through the associated educational and outreach activities, via graduate courses, undergraduate capstone projects, and K-12 outreach program, the project will contribute to a highly skilled workforce in this area of national need. The project will help diversity in cybersecurity workforce by engaging women and underrepresented minorities in research and educational activities. In addition, the project will significantly contribute to imparting hands-on cybersecurity training to industry professionals using the testbed platform. Both educational and training modules will be made available to a broader academic and industry communities. The overarching vision of this project is to transform the fault-resilient grid of today into an attack-resilient grid of the future. Towards achieving this vision, the goal of the project is to develop and evaluate algorithms and tools that will significantly advance the state-of-the-art cyber risk assessment, attack-defense modeling, and cyber contingency analysis. This goal will be accomplished by undertaking the following research tasks: (1) Develop fundamental game-theoretic formulations (single stage, multi-stage, Bayesian) for attack-defense modeling for the power grid using behavioral and learning models; (2) Develop a quantitative cyber risk assessment and mitigation methodology that capture all three components of risk -- namely, threats, vulnerabilities, and consequences -- using pragmatic game-theoretic formulations, and optimize the security investments to defend the grid against high-risk attacks; (3) Develop scalable techniques and tools for real-time operational planning using game-theoretic formulations to account for multiple contingencies arising due to coordinated cyber-attacks, and integrate them into a dynamic contingency analysis methodology as part of the Energy Management System (EMS); (4) Evaluate the effectiveness and scalability of the developed solutions and tools on Iowa State CPS security testbed environment using realistic attack-defense scenarios leveraging well documented power and cyber system topologies and synthetic attack traces and also leveraging Iowa State industry partnerships in Electric Power Research Center (EPRC) and Power System Research Center (PSERC).

Wearable exoskeletons are one of the primary advancements that help to alleviate the effects of spinal cord injury (SCI) including degenerative changes in organs of the body. Artificially stimulating the wearer's muscles to move his or her limbs has the additional benefit of maintaining musculature and improving circulation. The exoskeleton system developed in this project will use this "muscles first" approach with additional assistive power from electric motors on an as-needed basis. The major contribution of the project is that it will ensure stability of the person during standing and at normal walking speeds. The result will be that persons with SCI will be more comfortable standing and walking more erect and, therefore, be more socially engaged. The societal impact of this will be that persons with SCI will be better able to work and participate in social and leisure activities and in other behaviors associated with independent and productive lifestyles. In addition, Cleveland area high school students will be involved in the project and learn about human biomechanics and engineering methods. This project addresses how cyber physical walking systems (CPWS) can be designed to be safe, secure, and resilient despite a variety of unanticipated disturbances and how real-time dynamic control and behavior adaptation can be achieved in a diversity of environments. Specifically, a CPWS will be developed that seamlessly integrates: (1) a person who has a spinal cord injury (SCI) with intact and excitable lower motor nerves; (2) an exoskeleton with controllably locked/unlocked and/or passively damped joints; (3) DC motors for need-dependent joint power assistance; and (4) computational algorithms that continuously and automatically learn to improve standing and walking stability. In this "muscles first" approach, functional neural stimulation (FNS) provides most of the joint torques for walking and for maximum health benefits and, thus, as-needed assistive joint motors may be small and lightweight. The specific aims are 1) Assist the user's muscles on an as-needed basis and for high-bandwidth stability control by adding small, low passive-resistance motor/transmission pairs to our CPWS; 2) Develop computational algorithms for system estimation, machine learning and stability control for SCI users standing and walking with a CPWS while minimizing upper extremity effort; 3) Verify system performance with able-bodied individuals and assess upper extremity reduction and balance control in individuals with SCI using the CPWS for standing and ambulation.

Cyber-physical and Internet-of-Things (CPS/IoT) systems offer dramatic potential for revolutionizing many aspects of modern life by facilitating collection, analysis, and action on fine-grained sensor data. In both consumer-facing systems (e.g. smart locks, cameras, and thermostats) as well as infrastructure and industrial settings (e.g. devices to monitor factories or electricity distribution systems), CPS/IoT systems are already responsible for a wide range of safety-critical functions with significant security implications. CPS/IoT systems' correctness and security shortcomings have implications both for device users themselves, and more broadly across the Internet, due to malware attacks hosted by these devices. This project attacks the problem of verifying the correctness and security of CPS/IoT systems by developing design-time verification techniques to be used prior to deployment, as well as run-time verification techniques for systems in use. The project includes components to engage undergraduate students in research, and to improve the diversity of the computing workforce. The proposed research has two main thrusts. The first develops efficient, formal verification techniques for CPS/IoT Systems. These can be employed statically at design time or compile-time to comprehensively assess that state updates will occur in correct orderings based on design specifications provided by the designer or gleaned automatically from hardware design languages and software. The second explores hardware support for formal, dynamic IoT system verification. In particular, so-called ``lifeguard'' techniques can be employed to watch state updates in real-time and react to them with hardware or software error handlers as needed. This allows systems to maintain oversight over arbitrary CPS/IoT applications and help ensure their appropriate operation. A set of CPS/IoT verification tools to support design-time and compile-time verification and all hardware support designs and techniques developed will be released for broad open-source use.

This project aims to empower ordinary citizens to take charge in collecting real time environmental data that can be used to serve a common interest. The target application of the project is a cyber-physical system for detecting small amounts of explosive vapor in the air so as to protect large-area public gatherings. In this system, extremely low-cost explosive sensors, handed out free of charge, will be connected to the smart phones of the willing participants, effectively turning each one of them into a look-out sensor node. Although the primary application of the proposed cyber-physical system is explosive detection, problems with similar technical challenges include air pollution monitoring systems, pandemic prevention, fire and/or gas leak monitoring. Successful completion of this project will generate a plethora of new applications that target problems with the aim of reaching a common goal by leveraging computation, power, and communications capacities donated by willing participants. Understanding that interest in STEM (science, technology, engineering, math)-related careers begins in elementary school, the project will use a sensor-based system that aims at locating a heat source, as part of K-12 outreach activities that explore crowd-sourced data collection, processing, and scheduling. The researchers work regularly with undergraduate and high school students through Fulton Undergraduate Research Initiative (FURI), Barrett Summer Scholars (BSS), National Science Foundation-sponsored National Nanotechnology Infrastructure Network Research Experience for Undergraduates (NNIN REU), and Arizona State University's Summer Research Experience for High School Students program. Designing a system based on extremely low-cost sensors for crowd-sourced monitoring has several unique technical and scientific challenges that the project tackles. First, cost/power requirements and the need to detect tiny amounts of explosive vapor are at odds with each other. Second, the system will be designed to tolerate inevitable sensor inaccuracies and false positives/negatives in a stable manner. Third, since the entire system hinges on willing participation from the public, sensor operation will be made transparent to the user, and not create a negative user experience. Finally, privacy concerns of the users will be addressed by keeping them anonymous, and the security threats generated by this anonymity will be addressed.

Cyber-physical and Internet-of-Things (CPS/IoT) systems offer dramatic potential for revolutionizing many aspects of modern life by facilitating collection, analysis, and action on fine-grained sensor data. In both consumer-facing systems (e.g. smart locks, cameras, and thermostats) as well as infrastructure and industrial settings (e.g. devices to monitor factories or electricity distribution systems), CPS/IoT systems are already responsible for a wide range of safety-critical functions with significant security implications. CPS/IoT systems' correctness and security shortcomings have implications both for device users themselves, and more broadly across the Internet, due to malware attacks hosted by these devices. This project attacks the problem of verifying the correctness and security of CPS/IoT systems by developing design-time verification techniques to be used prior to deployment, as well as run-time verification techniques for systems in use. The project includes components to engage undergraduate students in research, and to improve the diversity of the computing workforce. The proposed research has two main thrusts. The first develops efficient, formal verification techniques for CPS/IoT Systems. These can be employed statically at design time or compile-time to comprehensively assess that state updates will occur in correct orderings based on design specifications provided by the designer or gleaned automatically from hardware design languages and software. The second explores hardware support for formal, dynamic IoT system verification. In particular, so-called ``lifeguard'' techniques can be employed to watch state updates in real-time and react to them with hardware or software error handlers as needed. This allows systems to maintain oversight over arbitrary CPS/IoT applications and help ensure their appropriate operation. A set of CPS/IoT verification tools to support design-time and compile-time verification and all hardware support designs and techniques developed will be released for broad open-source use.

The goal of this project is to leverage and improve upon the capabilities of honey bees as agricultural pollinators by incorporating them into Bio-Cyber Physical systems. Rapid advances are needed to aid a dwindling agricultural workforce, increase crop yield to sustain the growing population, and provide targeted crop care to limit the need for broad pesticide treatments. These challenges may well be addressed by autonomous mobile robots and sensor networks; unfortunately, agricultural landscapes represent vast, complicated, and dynamic environments that complicate long term operation. In contrast, social insects are capable of robust sustained operation in unpredictable environments far beyond what is possible with state-of-the-art artificial systems. Colonies of honey bees are of particular interest in this project, because they are the premiere agricultural pollinator bringing in over $150 billion annually. The U.S. has an estimated 2.4 million colonies, many of whom travel the country every summer to help pollinate monocrops such as almond and corn. A colony causes pollination by dispatching tens of thousands of scouts and foragers to survey and sample kilometer-wide areas around their hive. Thus, the colony as a whole accumulates vast information about the local agricultural landscape, bloom and dearth -- information that would be very informative if available to farmers and beekeepers. This project will leverage social insects as environmental indicators by piggybacking on their naturally existing capabilities. It involves sensors to record where bees focus their foraging activity, and mechanisms to stimulate additional foragers. This project will impact: 1) ultra-low power electronics and sensing, 2) probabilistic inference from large scale distributed data sources, 3) feedback control of biohybrid systems, and 4) gains to apiculture and entomology. The proposed bio-hybrid technology may further inform models of how bees forage in natural versus cultivated areas, and may lead to new insights on design of agricultural multi-use landscapes for improved yield. Overall, this research will improve engineers' understanding of Bio-Cyber Physical Systems able to monitor and affect the environment, and may be applicable to scenarios including search and rescue, detection of chemical spills, and targeted pollination. To harness the capabilities of a bee colony while still providing control and sensing, the proposed work specifically involves 1) novel submillimeter flight recorders with visual scene capture and analysis, thermal and mechanical sensors, a clock, storage, processing, photovoltaic chargers and short range communications; 2) algorithms and models to estimate foraging maps, relying on bee motion models and feature extraction, merging probability density functions of observed landmarks from thousands of flights; and 3) feedback control via a bee-mimicking shaker device to recruit foragers, in turn eliciting data collection and pollination, e.g. during brief spouts of bloom that would otherwise go unnoticed by the colony. This research represents a transformative step towards a new frontier in Bio-Cyber Physical Systems, improving upon the abilities of social insects to sense and interact with the physical world, while providing data acquisition and control on par with explicitly engineered systems.

Energy storage and power distribution play an integral part in the engineered systems that play critical roles in people's everyday lives, including transportation, utility, health, and security. In today's cyber-physical platforms, however, the generation, storage, allocation, and distribution of energy among modules is often managed in a haphazard and rigid manner that is fixed at the system design stage. The limitations of existing power management methods are clearly evident in highly-integrated meso-scale systems, which range from mobile devices to large installations such as the International Space Station. The power semantics of these meso-scale systems fall in between those of macro-scale power grids and micro-scale on-chip power management, resulting in a significant solution void. This research project aims to fill that void by establishing an agile, yet resilient, framework to design and manage power distribution and energy storage in cyber-physical systems. The broader impacts of this project will not only transform power delivery capabilities in emerging technologies such as the next generation of electric and hybrid autonomous vehicles, but also enrich inter-disciplinary education by bridging hardware-oriented power electronics design with control, system software, and application development, through curriculum integration and outreach programs. This research will develop a principled approach towards two main goals: modularizing the management of power semantics in meso-scale cyber-physical systems, and orchestrating the power-related system-wide interactions among heterogeneous modules. We begin by introducing an innovative equivalence between the management of power distribution and the optimization of energy packet delivery. This new problem formulation allows us to re-imagine the power architecture by incorporating malleable power modules as smart energy routers, connecting and buffering bidirectional power flows between diverse functional components such as motors, processors, and sensors. This research will develop a novel approach to efficient delivery of energy packets, which will allow reasoning about optimality and trade-offs among power and performance semantics holistically. This project will also establish a new intelligent coordination framework based on formal methods, for off-line generation of on-line interfaces among power modules, aiming to orchestrate exchanges of power among modules at a full-system level, even in the face of variability and model uncertainty. This modular power flow orchestration framework is a step towards a theory of modular smart ubiquitous cyber-physical devices, empowering a paradigm shift in how next-generation systems with new semantic objectives such as long-term sustainable autonomy can be built.

The project will research a new process for manufacturing large-scale libraries of synthetic DNA oligonucleotides, which are widely used in genomics research and are now being considered as a medium for long-term archival data storage. The current price for synthesizing DNA using microarray technology is 10 cents per base, equivalent to about $3,500 per Megabyte of storage. This project attempts to reduce the cost of DNA synthesis from 10 cents to around 0.007 cents per base using computer-controlled, high-throughput sorting. The DNA synthesis method will also include automatic data encryption. While the development of conventional digital data storage technologies (e.g., hard disk, flash memory) preceded the integration of encryption, pursuing encryption as part of the DNA synthesis process ensures that future DNA-based archival storage modalities will be robustly protected from tampering. The project builds on systems engineering principles and the foundations of Cyber-Physical Systems (CPS). DNA will be synthesized on a laser-light activated microtransponder chip (p-Chip) that transmits a unique ID by radio frequency (RF) or optical signaling, and can be used as a solid-phase support for DNA synthesis. Of particular importance is the design of a high-throughput microfluidic sorter/manifold, that can rapidly sort p-Chips in real-time, delivering them to reservoirs which apply the appropriate DNA chemistry to synthesize and append the next oligonucleotide to the sequence being grown on each p-Chip. Three 12-inch silicon production wafers carry enough p-Chips to synthesize a library of 5,000,000 unique DNA sequences, or a genome of 300,000,000 base pairs. p-Chips are chemically inert, compatible with DNA synthesis, and dense enough to allow high-speed mechanical separation. The intellectual significance of the work involves: (1) investigation of fluid modeling algorithms for p-Chips flowing through the high-speed microfluidic p-Chip sorter/manifold, including the needed corrections to the computational fluid flow models produced by commercial software, (2) investigation of a co-design process for fluidic CPS and its application to the creation of a sorter/manifold for current-generation (500 x 500 x 100 cubic micrometers) and next-generation (50 x 50 x 100 cubic micrometers) p-Chips, (3) real time software and/or Field Programmable Gate Array (FPGA) control for the sorter/manifold to enable ultra-high throughput DNA synthesis, (4) support for encrypted DNA synthesis, and (5) integration of the sorter/manifold and control mechanism into a commercial DNA synthesizer.