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 confluence of new networked sensing technologies (e.g., cameras), distributed computational resources (e.g., cloud computing), and algorithmic advances (e.g., computer vision) are offering new and exciting opportunities for solving a variety of new problems that are of societal importance including emergency response, disaster recovery, surveillance, and transportation. Solutions to this new class of problems, referred to as "situation awareness" applications, include surveillance via large-scale distributed camera networks and personalized traffic alerts in vehicular networks using road and traffic sensing. A breakthrough in system software technology is needed to meet the challenges posed by these applications since they are latency-sensitive, data intensive, involve heavy-duty processing, and must run 24x7 while dealing with the vagaries of the physical world. This project aims to make such a breakthrough, through new distributed programming idioms and resource allocation strategies. To better identify the challenges posed by situation awareness applications, the project includes experimental deployment of the new technologies in partnership with the City of Baton Rouge, Louisiana. The central activity is to develop appropriate system abstractions for design of situation awareness applications and encapsulate them in distributed programming idioms for domain experts (e.g., vision researchers). The resulting programming framework allows association of critical attributes such as location, time, and mobility with sensed data to reason about causal events along these axes. To meet the latency constraints of these applications, the project develops geospatial resource allocation mechanisms that complement and support the distributed programming idioms, extending the utility-computing model of cloud computing to the edge of the network. Since the applications often have to work with inexact knowledge of what is happening in the physical environment, owing to limitations of the distributed sensing sources, the project also investigates system support for application-specific information fusion and spatio-temporal analyses to increase the quality of results. Efforts toward development of a future cyber-physical systems workforce include creation of a new multidisciplinary curriculum around situation awareness, exploration of new immersive learning pedagogical styles, and mentoring and providing research experience to undergraduate students through research experiences and internships aimed at increasing participation of women and minorities.

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.

Designing semi-autonomous networks of miniature robots for inspection of bridges and other large civil infrastructure According to the U.S. Department of Transportation, the United States has 605102 bridges of which 64% are 30 years or older and 11% are structurally deficient. Visual inspection is a standard procedure to identify structural flaws and possibly predict the imminent collapse of a bridge and determine effective precautionary measures and repairs. Experts who carry out this difficult task must travel to the location of the bridge and spend many hours assessing the integrity of the structure. The proposal is to establish (i) new design and performance analysis principles and (ii) technologies for creating a self-organizing network of small robots to aid visual inspection of bridges and other large civilian infrastructure. The main idea is to use such a network to aid the experts in remotely and routinely inspecting complex structures, such as the typical girder assemblage that supports the decks of a suspension bridge. The robots will use wireless information exchange to autonomously coordinate and cooperate in the inspection of pre-specified portions of a bridge. At the end of the task, or whenever possible, they will report images as well as other key measurements back to the experts for further evaluation. Common systems to aid visual inspection rely either on stationary cameras with restricted field of view, or tethered ground vehicles. Unmanned aerial vehicles cannot access constricted spaces and must be tethered due to power requirements and the need for uninterrupted communication to support the continual safety critical supervision by one or more operators. In contrast, the system proposed here would be able to access tight spaces, operate under any weather, and execute tasks autonomously over long periods of time. The fact that the proposed framework allows remote expert supervision will reduce cost and time between inspections. The added flexibility as well as the increased regularity and longevity of the deployments will improve the detection and diagnosis of problems, which will increase safety and support effective preventive maintenance. This project will be carried out by a multidisciplinary team specialized in diverse areas of cyber-physical systems and robotics, such as locomotion, network science, modeling, control systems, hardware sensor design and optimization. It involves collaboration between faculty from the University of Maryland (UMD) and Resensys, which specializes in remote bridge monitoring. The proposed system will be tested in collaboration with the Maryland State Highway Administration, which will also provide feedback and expertise throughout the project. This project includes concrete plans to involve undergraduate students throughout its duration. The investigators, who have an established record of STEM outreach and education, will also leverage on exiting programs and resources at the Maryland Robotics Center to support this initiative and carry out outreach activities. In order to make student participation more productive and educational, the structure of the proposed system conforms to a hardware architecture adopted at UMD and many other schools for the teaching of undergraduate courses relevant to cyber-physical systems and robotics. This grant will support research on fundamental principles and design of robotic and cyber-physical systems. It will focus on algorithm design for control and coordination, network science, performance evaluation, microfabrication and system integration to address the following challenges: (i) Devise new locomotion and adhesion principles to support mobility within steel and concrete girder structures. (ii) Investigate the design of location estimators, omniscience and coordination algorithms that are provably optimal, subject to power and computational constraints. (iii) Methods to design and analyze the performance of energy-efficient communication protocols to support robot coordination and localization in the presence of the severe propagation barriers caused by metal and concrete structures of a bridge.

This Cyber-Physical Systems (CPS) award supports research to enable the automated monitoring of building and infrastructure construction projects. The purpose of construction monitoring is to provide developers, contractors, subcontractors, and tradesmen with the information they need to easily and quickly make project control decisions. These decisions have a direct impact on the overall efficiency of a construction project. Given that construction is a $800 billion industry, gains in efficiency could lead to enormous cost savings, benefiting both the U.S. economy and society. In particular, both construction cost and delivery time could be significantly reduced by automated tools to assess progress towards completion (progress monitoring) and how construction resources are being utilized (activity monitoring). These tools will be provided by advances in the disciplines of computer vision, robotics, and construction management. The interdisciplinary nature of this project will create synergy among these disciplines and will positively influence engineering education. Partnerships with industry will also ensure that these advances have a positive impact on construction practice. The process of construction monitoring involves data collection, analysis, and reporting. Research will address the existing scientific challenges to automating these three activities. Data collection will be automated by recording video with aerial robots and a network of cameras. Key research objectives are to derive planning algorithms that guarantee complete coverage of a construction site and to derive vision-based control algorithms that enable robust placement and retrieval of cameras. Analysis will be automated with a digital building information model with respect to which construction resources can be tracked. Key research objectives are to improve the efficiency and reliability of image-based reconstruction, to recognize material properties as well as geometry, to establish a formal language for representing construction activities, and to extend a parts-based approach for automated activity recognition. Reporting will be automated with a ubiquitous display of the digital building information model. Key research objectives are to formalize a constraint construction ontology with associated classification mechanisms and allow for systematic earned value analysis of construction progress. Experimental validation will focus on monitoring construction of substructure and superstructure skeletal elements in buildings and infrastructure systems as well as the associated earth-moving, concrete placement, and steel erection activities that are common in construction projects.

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.

This project aims to enable cyber-physical systems that can be worn on the body in order to one day allow their users to touch, feel, and manipulate computationally simulated three-dimensional objects or digital data in physically realistic ways, using the whole hand. It will do this by precisely measuring touch and movement-induced displacements of the skin in the hand, and by reproducing these signals interactively, via new technologies to be developed in the project. The resulting systems will offer the potential to impact a wide range of human activities that depend on touch and interaction with the hands. The project seeks to enable new applications for wearable cyber physical interfaces that may have broad applications in health care, manufacturing, consumer electronics, and entertainment. Although human interactive technologies have advanced greatly, current systems employ only a fraction of the sensorimotor capabilities of their users, greatly limiting applications and usability. The development of whole-hand haptic interfaces that allow their wearers to feel and manipulate digital content has been a longstanding goal of engineering research, but has remained far from reality. The reason can be traced to the difficulty of reproducing or even characterizing the complex, action-dependent stimuli that give rise to touch sensations during everyday activities. This project will pioneer new methods for imaging complex haptic stimuli, consisting of movement dependent skin strain and contact-induced surface waves propagating in skin, and for modeling the dependence of these signals on hand kinematics during grasping. It will use the resulting fundamental advances to catalyze the development of novel wearable CPS, in the form of whole-hand haptic interfaces. The latter will employ surface wave and skin strain feedback to supply haptic feedback to the hand during interaction with real and computational objects, enabling a range of new applications in VR. The project will be executed through research in three main research areas. In the first, it will utilize novel contact and non-contact techniques based on data acquired through on-body sensor arrays to measure whole-hand mechanical stimuli and grasping kinematics at high spatial and temporal resolution. In a second research area, it will undertake data-driven systems modeling and analysis of statistical contingencies between the kinematic and cutaneous sensed during everyday activities. In a third research area, it will engineer and perceptually evaluate novel cyber physical systems consisting of haptic interfaces for whole hand interaction. In order to further advance the applications of these systems in medicine, through a collaboration with the Drexel College of Medicine, the project will develop new methods for assessing clinical skills of palpation during medical examination, with the aim of improving the efficacy of what is often the first, most common, and best opportunity for diagnosis, using physician's own sense of touch.

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.

More than one million people including many wounded warfighters from recent military missions are living with lower-limb amputation in the United States. This project will design wearable body area sensor systems for real-time measurement of amputee's energy expenditure and will develop computer algorithms for automatic lower-limb prosthesis optimization. The developed technology will offer a practical tool for the optimal prosthetic tuning that may maximally reduce amputee's energy expenditure during walking. Further, this project will develop user-control technology to support user's volitional control of lower-limb prostheses. The developed volitional control technology will allow the prosthesis to be adaptive to altered environments and situations such that amputees can walk as using their own biological limbs. An optimized prosthesis with user-control capability will increase equal force distribution on the intact and prosthetic limbs and decrease the risk of damage to the intact limb from the musculoskeletal imbalance or pathologies. Maintenance of health in these areas is essential for the amputee's quality of life and well-being. Student participation is supported. This research will advance Cyber-Physical Systems (CPS) science and engineering through the integration of sensor and computational technologies for the optimization and control of physical systems. This project will design body area sensor network systems which integrate spatiotemporal information from electromyography (EMG), electroencephalography (EEG) and inertia measurement unit (IMU) sensors, providing quantitative, real-time measurements of the user's physical load and mental effort for personalized prosthesis optimization. This project will design machine learning technology-based, automatic prosthesis parameter optimization technology to support in-home prosthesis optimization by users themselves. This project will also develop an EEG-based, embedded computing-supported volitional control technology to support user?s volitional control of a prosthesis in real-time by their thoughts to cope with altered situations and environments. The technical advances from this project will provide wearable and wireless body area sensing solutions for broader applications in healthcare and human-CPS interaction applications. The explored computational methods will be broadly applicable for real-time, automatic target recognition from spatiotemporal, multivariate data in CPS-related communication and control applications. This synergic project will be implemented under multidisciplinary team collaboration among computer scientists and engineers, clinicians and prosthetic industry engineers. This project will also provide interdisciplinary, CPS relevant training for both undergraduate and graduate students by integrating computational methods with sensor network, embedded processors, human physical and mental activity recognition, and prosthetic control.

This project represents a cross-disciplinary collaborative research effort on developing rigorous, closed-loop approaches for designing, simulating, and verifying medical devices. The work will open fundamental new approaches for radically accelerating the pace of medical device innovation, especially in the sphere of cardiac-device design. Specific attention will be devoted to developing advanced formal methods-based approaches for analyzing controller designs for safety and effectiveness; and devising methods for expediting regulatory and other third-party reviews of device designs. The project team includes members with research backgrounds in computer science, electrical engineering, biophysics, and cardiology; the PIs will use a coordinated approach that balances theoretical, experimental and practical concerns to yield results that are intended to transform the practice of device design while also facilitating the translation of new cardiac therapies into practice. The proposed effort will lead to significant advances in the state of the art for system verification and cardiac therapies based on the use of formal methods and closed-loop control and verification. The animating vision for the work is to enable the development of a true in silico design methodology for medical devices that can be used to speed the development of new devices and to provide greater assurance that their behaviors match designers' intentions, and to pass regulatory muster more quickly so that they can be used on patients needing their care. The scientific work being proposed will serve this vision by providing mathematically robust techniques for analyzing and verifying the behavior of medical devices, for modeling and simulating heart dynamics, and for conducting closed-loop verification of proposed therapeutic approaches. The acceleration in medical device innovation achievable as a result of the proposed research will also have long-term and sustained societal benefits, as better diagnostic and therapeutic technologies enter into the practice of medicine more quickly. It will also yield a collection of tools and techniques that will be applicable in the design of other types of devices. Finally, it will contribute to the development of human resources and the further inclusion of under-represented groups via its extensive education and outreach programs, including intensive workshop experiences for undergraduates.