Airborne networking, unlike the networking of fixed sensors, mobile devices, and slowly-moving vehicles, is very challenging because of the high mobility, stringent safety requirements, and uncertain airspace environment. Airborne networking is important because of the growing complexity of the National Airspace System with the integration of unmanned aerial vehicles (UAVs). This project develops an innovative new theoretical framework for cyber-physical systems (CPS) to enable airborne networking, which utilizes direct flight-to-to-flight communication for flexible information sharing, safe maneuvering, and coordination of time-critical missions. This project uses an innovative co-design approach that exploits the mutual benefits of networking and decentralized mobility control in an uncertain heterogeneous environment. The approach departs from the usual perspective that views physical mobility as communication constraints, communication as constraints for decentralized mobility control, and uncertain environment as constraints for both. Instead, approach taken here proactively exploits the constraints, uncertainty, and new structures with information to enable high-performance designs. The features of the co-design such as scalability, fast response, trackability, and robustness to uncertainty advance the core CPS science on decision-making for large-scale networks under uncertainty. The technological advances developed in this research will contribute to multiple fields, including mobile networking, decentralized control, experiment design, and general real-time decision making under uncertainty for CPS. Technology transfer will be pursued through close collaboration with industries and national laboratories. This novel research direction will also serve as a unique backdrop to inspire the CPS workforce. New teaching materials will benefit the future CPS workforce by equipping them with a knowledge base in networking and control. Broad outreach and dissemination activities that involve undergraduate student societies, K-12 school teaching, and public events, all stemming from the PI's current efforts, will be enhanced.

This project advances the scientific knowledge on design methods for improving the resilience of civil infrastructures to disruptions. To improve resilience, critical services in civil infrastructure sectors must utilize new diagnostic tools and control algorithms that ensure survivability in the presence of both security attacks and random faults, and also include the models of incentives of human decision makers in the design process. This project will develop a practical design toolkit and platform to enable the integration of resiliency-improving control tools and incentive schemes for Cyber-Physical Systems (CPS) deployed in civil infrastructures. Theory and algorithms will be applied to assess resiliency levels, select strategies to improve performance, and provide reliability and security guarantees for sector-specific CPS functionalities in water, electricity distribution and transportation infrastructures. The main focus is on resilient design of network control functionalities to address problems of incident response, demand management, and supply uncertainties. More broadly, the knowledge and tools from this project will influence CPS designs in water, transport, and energy sectors, and also be applicable to other systems such as supply-chains for food, oil and gas. The proposed platform will be used to develop case studies, test implementations, and design projects for supporting education and outreach activities. Current CPS deployments lack integrated components designed to survive in uncertain environments subject to random events and the actions of strategic entities. The toolkit (i) models the propagation of disruptions due to failure of cyber-physical components, (ii) detects and responds to both local and network-level failures, and (iii) designs incentive schemes that improve aggregate levels of public good (e.g., decongestion, security), while accounting for network interdependencies and private information among strategic entities. The validation approach uses real-world data collected from public sources, test cases developed by domain experts, and simulation software. These tools are integrated to provide a multi-layer design platform, which explores the design space to synthesize solutions that meet resiliency specifications. The platform ensures that synthesized implementations meet functionality requirements, and also estimates the performance guarantees necessary for CPS resilience. This modeling, validation, exploration, and synthesis approach provides a scientific basis for resilience engineering. It supports CPS education by providing a platform and structured workflow for future engineers to approach and appreciate implementation realities and socio-technical constraints.

Every year around 30,000 fatalities and 2.2 million injuries happen on US roads. The problem is compounded with huge economic losses due to traffic congestions. Advances in Cooperative Vehicle Efficiency and Safety (CVES) systems promise to significantly reduce the human and economic cost of transportation. However, large scale deployment of such systems is impeded by significant technical and scientific gaps, especially when it comes to achieving real-time and high accuracy situational awareness for cooperating vehicles. This CAREER project aims at closing these gaps through developing fundamental information networking methodologies for coordinated control of automated systems. These methodologies will be based on the innovative concept of modeled knowledge propagation. In addition, the educational component of this project integrates interdisciplinary Cyber-Physical Systems (CPS) subjects on the design of automated networked systems into graduate and undergraduate training modules. For robust operation, CVES systems require each vehicle to have reliable real-time awareness of the state of other coordinated vehicles. This project addresses the critical need for robust control-oriented situational awareness by developing a multi-resolution information networking methodology that is model- and context-aware. The approach is to develop the novel concepts of model communication and its derived multi-resolution networking. Context-aware model-communication relies on transmission and synchronization of models (e.g., stochastic hybrid system structures and parameters) instead of raw measurements. This allows for high fidelity synchronization of dynamical models of CVES over networks. Multi-resolution networking concept is enabled through scalable representations of models. Multi resolution models allow in-network adaptation of model fidelity to available network resources. The result is robustness of CVES to network service variability. The successful deployment of CVES, even partially, will provide significant societal benefits through reduced traffic accidents and improved efficiency. This project will enable large scale CVES deployment by addressing its scalability challenge. In addition, methodologies developed in this project will be crucial to emerging autonomous vehicles, which are also expected to coordinate their actions over communication networks. The fundamental research outcomes on knowledge propagation through network synchronization of dynamical models will be broadly applicable in other CPS domains such as smart grid. The educational component of this project will target training of CPS researchers and engineers on subjects in intelligent transportation and energy systems.

Brain-computer interfaces (BCIs) are cyber-physical systems (CPSs) that record human brain waves and translate them into the control commands for external devices such as computers and robots. They may allow individuals with spinal cord injury (SCI) to assume direct brain control of a lower extremity prosthesis to regain the ability to walk. Since the lower extremity paralysis due to SCI leads to as much as $50 billion of health care cost each year in the US alone, the use of a BCI-controlled lower extremity prosthesis to restore walking can have a significant public health impact. Recent results have demonstrated that a person with paraplegia due to SCI can use a non-invasive BCI to regain basic walking. While encouraging, this BCI is unlikely to become a widely adopted solution since the poor signal quality of non-invasively recorded brain waves may lead to unreliable BCI operation. Moreover, lengthy and tedious mounting procedures of the non-invasive BCI systems are impractical. A permanently implantable BCI CPS can address these issues, but critical challenges must be overcome to achieve this goal, including the elimination of protruding electronics and reliance on an external computer for brain signal processing. The goal of this study is to develop a benchtop version of a fully implantable BCI CPS, capable of acquiring electrocorticogram signals, recorded directly from the surface of the brain, and analyzing them internally to enable direct brain control of a robotic gait exoskeleton (RGE) for walking. The BCI CPS will be designed as a low-power system with revolutionary adaptive power management in order to meet stringent heat and power consumption constraints for future human implantation. Comprehensive measurements and benchtop tests will ensure proper function of BCI CPS. Finally, the system will be integrated with an RGE, and its ability to facilitate brain-controlled walking will be tested in a small group of human subjects. The successful completion of this project will have broad bioengineering and scientific impact. It will revolutionize medical device technology by minimizing power consumption and heat production while enabling complex operations to be performed. The study will also help deepen the understanding of how the human brain controls walking, which has long been a mystery to neuroscientists. Finally, this study?s broader impact is to promote education and lifelong learning in engineering students and the community, broaden the participation of underrepresented groups in engineering, and increase the scientific literacy of persons with disabilities. Research opportunities will be provided to (under-)graduate students. Their findings will be broadly disseminated and integrated into teaching activities. To inspire underrepresented K-12 and community college students to pursue higher education in STEM fields, and to increase the scientific literacy of persons with disabilities, outreach activities will be undertaken in the form of live scientific exhibits and actual BCI demonstrations. Recent results have demonstrated that a person with paraplegia due to SCI can use an electroencephalogram (EEG)-based BCI to regain basic walking. While encouraging, this EEG-based BCI is unlikely to become a widely adopted solution due to EEG?s inherent noise and susceptibility to artifacts, which may lead to unreliable operation. Also, lengthy and tedious EEG (un-)mounting procedures are impractical. A permanently implantable BCI CPS can address these issues, but critical CPS challenges must be overcome to achieve this goal, including the elimination of protruding electronics and reliance on an external computer for neural signal processing. The goal of this study is to implement a benchtop analogue of a fully implantable BCI CPS, capable of acquiring high-density (HD) electrocorticogram (ECoG) signals, and analyzing them internally to facilitate direct brain control of a robotic gait exoskeleton (RGE) for walking. The BCI CPS will be designed as a low-power modular system with revolutionary adaptive power management in order to meet stringent heat dissipation and power consumption constraints for future human implantation. The first module will be used for acquisition of HD-ECoG signals. The second module will internally execute optimized BCI algorithms and wirelessly transmit commands to an RGE for walking. System and circuit-level characterizations will be conducted through comprehensive measurements. Benchtop tests will ensure the proper system function and conformity to biomedical constraints. Finally, the system will be integrated with an RGE, and its ability to facilitate brain-controlled walking will be tested in a group of human subjects.The successful completion of this project will have broad bioengineering and scientific impact. It will revolutionize medical device technology by minimizing power consumption and heat dissipation while enabling complex algorithms to be executed in real time. The study will also help deepen the physiological understanding of how the human brain controls walking. This study will promote education and lifelong learning in engineering students and the community, broaden the participation of underrepresented groups in engineering, and increase the scientific literacy of persons with disabilities. Research opportunities will be provided to under-graduate students. Their findings will be broadly disseminated and integrated into teaching activities. To inspire underrepresented K-12 and community college students to pursue higher education in STEM fields, and to increase the scientific literacy of persons with disabilities, outreach activities will be undertaken in the form of live scientific exhibits and actual BCI demonstrations.

Cyber physical systems extend the range of human capabilities in an increasing number of areas with high societal and economic impact, such as smart energy, intelligent transportation, advanced manufacturing, health technology, and the environment. Their successful operation requires the close integration of communication, sensing, actuation, control, and computation. However, advances in these fields have not always been well coordinated. Information theory, for instance, studies how to compress and protect information communicating over noisy channels, while in many control applications communication is abstracted as being instantaneous and reliable. Information theory states that long codes are desirable to protect data against channel noise, but for control applications long delays are not acceptable. On the other hand, triggered control takes an opportunistic approach to decide when actions should be taken to make the system operate efficiently, but largely ignores the constraints imposed by communication. This proposal contributes to the development of a common theoretical framework for control and communication that merges information theory and triggered control to design robust and efficient protocols for the operation of cyber physical systems in real-world scenarios. Such a synergy can have a tremendous impact in the societal settings mentioned above, and at the same time will enable education of students and researchers to prepare themselves in this emerging area of technology. The aim of the project is to develop a synergistic approach to solving the problem of control under communication constraints and/or unreliable communication channels. The approaches to state-triggered control and information-theoretic control individually address different and somewhat complementary aspects of the problem. Therefore, by leveraging the strengths of the two approaches superior and more complete solutions to the problem may be designed. An information-theoretic approach to providing data rate theorems can be used to enrich state-triggered strategies to prescribe both when and what to transmit, as well as to quantify the average usage of the communication channel. Similarly, existing control strategies for unreliable and stochastic communication channels can be enriched by considering triggering mechanisms as additional communication constraints to be accounted for in the feedback loop while designing the communication channel.

Advances in technology mean that computer-controlled physical devices that currently still require human operators, such as automobiles, trains, airplanes, and medical treatment systems, could operate entirely autonomously and make rational decisions on their own. Autonomous cars and drones are a concrete and highly publicized face of this dream. Before this dream can be realized we must address the need for safety - the guaranteed absence of undesirable behaviors emerging from autonomy. Highly publicized technology accidents such as rocket launch failures, uncontrolled exposure to radiation during treatment, aircraft automation failures and unintended automotive accelerations serve as warnings of what can happen if safety is not adequately addressed in the design of such cyber-physical systems. One approach for safety analysis is the use of software tools that apply formal logic to prove the absence of undesired behavior in the control software of a system. In prior work, this approach this been proven to work for simple controller software that is generated automatically by tools from abstract models like Simulink diagrams. However, autonomous decision making requires more complex software that is able to solve optimization problems in real time. Formal verification of control software that includes such optimization algorithms remains an unmet challenge. The project SORTIES (Semantics of Optimization for Real Time Intelligent Embedded Systems) draws upon expertise in optimization theory, control theory, and computer science to address this challenge. Beginning with the convergence properties of convex optimization algorithms, SORTIES examines how these properties can be automatically expressed as inductive invariants for the software implementation of the algorithms, and then incorporates these properties inside the source code itself as formal annotations which convey the underlying reasoning to the software engineer and to existing computer-aided verification tools. The SORTIES goal is an open-source-semantics-carrying autocoder, which takes an optimization algorithm and its convergence properties as input, and produces annotated, verifiable code as output. The demonstration of the tool on several examples, such as a Mars lander, an aircraft avionics system, and a jet engine controller, shows that the evidence of quality produced by annotations is fully compatible with its application to truly functional products. Project research is integrated with education through training of "tri-lingual" professionals, who are equally conversant in system operation, program analysis, and the theory of control and optimization.

Tracking Fish Movement with a School of Gliding Robotic Fish This project is focused on developing the technology for continuously tracking the movement of live fish implanted with acoustic tags, using a network of relatively inexpensive underwater robots called gliding robotic fish. The research addresses two fundamental challenges in the system design: (1) accommodating significant uncertainties due to environmental disturbances, communication delays, and apparent randomness in fish movement, and (2) balancing competing objectives (for example, accurate tracking versus long lifetime for the robotic network) while meeting multiple constraints on onboard computing, communication, and power resources. Fish movement data provide insight into choice of habitats, migratory routes, and spawning behavior. By advancing the state of the art in fish tracking technology, this project enables better-informed decisions for fishery management and conservation, including control of invasive species, restoration of native species, and stock assessment for high-valued species, and ultimately contributes to the sustainability of fisheries and aquatic ecosystems. By advancing the coordination and control of gliding robotic fish networks and enabling their operation in challenging environments such as the Great Lakes, the project also facilitates the practical adoption of these robotic systems for a myriad of other applications in environmental monitoring, port surveillance, and underwater structure inspection. The project enhances several graduate courses at Michigan State University, and provides unique interdisciplinary training opportunities for students including those from underrepresented groups. Outreach activities, including robotic fish demos, museum exhibits, teacher training, and "Follow That Fish" smartphone App, are specifically designed to pique the interest of pre-college students in science and engineering. The goal of this project is to create an integrative framework for the design of coupled robotic and biological systems that accommodates system uncertainties and competing objectives in a rigorous and holistic manner. This goal is realized through the pursuit of five tightly coupled research objectives associated with the application of tracking and modeling fish movement: (1) developing new robotic platforms to enable underwater communication and acoustic tag detection, (2) developing robust algorithms with analytical performance assurance to localize tagged fish based on time-of-arrival differences among multiple robots, (3) designing hidden Markov models and online model adaptation algorithms to capture fish movement effectively and efficiently, (4) exploring a two-tier decision architecture for the robots to accomplish fish tracking, which incorporates model-predictions of fish movement, energy consumption, and mobility constraints, and (5) experimentally evaluating the design framework, first in an inland lake for localizing or tracking stationary and moving tags, and then in Thunder Bay, Lake Huron, for tracking and modeling the movement of lake trout during spawning. This project offers fundamental insight into the design of robust robotic-physical-biological systems that addresses the challenges of system uncertainties and competing objectives. First, a feedback paradigm is presented for tight interactions between the robotic and biological components, to facilitate the refinement of biological knowledge and robotic strategies in the presence of uncertainties. Second, tools from estimation and control theory (e.g., Cramer-Rao bounds) are exploited in novel ways to analyze the performance limits of fish tracking algorithms, and to guide the design of optimal or near-optimal tradeoffs to meet multiple competing objectives while accommodating onboard resource constraints. On the biology side, continuous, dynamic tracking of tagged fish with robotic networks represents a significant step forward in acoustic telemetry, and results in novel datasets and models for advancing fish movement ecology.

Advances in technology mean that computer-controlled physical devices that currently still require human operators, such as automobiles, trains, airplanes, and medical treatment systems, could operate entirely autonomously and make rational decisions on their own. Autonomous cars and drones are a concrete and highly publicized face of this dream. Before this dream can be realized we must address the need for safety - the guaranteed absence of undesirable behaviors emerging from autonomy. Highly publicized technology accidents such as rocket launch failures, uncontrolled exposure to radiation during treatment, aircraft automation failures and unintended automotive accelerations serve as warnings of what can happen if safety is not adequately addressed in the design of such cyber-physical systems. One approach for safety analysis is the use of software tools that apply formal logic to prove the absence of undesired behavior in the control software of a system. In prior work, this approach this been proven to work for simple controller software that is generated automatically by tools from abstract models like Simulink diagrams. However, autonomous decision making requires more complex software that is able to solve optimization problems in real time. Formal verification of control software that includes such optimization algorithms remains an unmet challenge. The project SORTIES (Semantics of Optimization for Real Time Intelligent Embedded Systems) draws upon expertise in optimization theory, control theory, and computer science to address this challenge. Beginning with the convergence properties of convex optimization algorithms, SORTIES examines how these properties can be automatically expressed as inductive invariants for the software implementation of the algorithms, and then incorporates these properties inside the source code itself as formal annotations which convey the underlying reasoning to the software engineer and to existing computer-aided verification tools. The SORTIES goal is an open-source-semantics-carrying autocoder, which takes an optimization algorithm and its convergence properties as input, and produces annotated, verifiable code as output. The demonstration of the tool on several examples, such as a Mars lander, an aircraft avionics system, and a jet engine controller, shows that the evidence of quality produced by annotations is fully compatible with its application to truly functional products. Project research is integrated with education through training of "tri-lingual" professionals, who are equally conversant in system operation, program analysis, and the theory of control and optimization.

The project investigates a formal verification framework for artificial pancreas (AP) controllers that automate the delivery of insulin to patients with type-1 diabetes (T1D). AP controllers are safety critical: excessive insulin delivery can lead to serious, potentially fatal, consequences. The verification framework under development allows designers of AP controllers to check that their control algorithms will operate safely and reliably against large disturbances that include patient meals, physical activities, and sensor anomalies including noise, delays, and sensor attenuation. The intellectual merits of the project lie in the development of state-of-the-art formal verification tools, that reason over mathematical models of the closed-loop including external disturbances and insulin-glucose response. These tools perform an exhaustive exploration of the closed loop system behaviors, generating potentially adverse situations for the control algorithm under verification. In addition, automatic techniques are being investigated to help AP designers improve the control algorithm by tuning controller parameters to eliminate harmful behaviors and optimize performance. The broader significance and importance of the project are to minimize the manual testing effort for AP controllers, integrate formal tools in the certification process, and ultimately ensure the availability of safe and reliable devices to patients with type-1 diabetes. The framework is made available to researchers who are developing AP controllers to help them verify and iteratively improve their designs. The team is integrating the research into the educational mission by designing hands-on courses to train undergraduate students in the science of Cyber-Physical Systems (CPS) using the design of AP controllers as a motivating example. Furthermore, educational material that explains the basic ideas, current challenges and promises of the AP concept is being made available to a wide audience that includes patients with T1D, their families, interested students, and researchers. The research is being carried out collaboratively by teams of experts in formal verification for Cyber-Physical Systems, control system experts with experience designing AP controllers, mathematical modeling experts, and clinical experts who have clinically evaluated AP controllers. To enable the construction of the verification framework from the current state-of-the-art verification tools, the project is addressing major research challenges, including (a) building plausible mathematical models of disturbances from available clinical datasets characterizing human meals, activity patterns, and continuous glucose sensor anomalies. The resulting models are integrated in a formal verification framework; (b) simplifying existing models of insulin glucose response using smaller but more complex delay differential models; (c) automating the process of abstracting the controller implementation for the purposes of verification; (d) producing verification results that can be interpreted by control engineers and clinical researchers without necessarily understanding formal verification techniques; and (e) partially automating the process of design improvements to potentially eliminate severe faults and improve performance. The framework is evaluated on a set of promising AP controller designs that are currently under various stages of clinical evaluation.