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 focuses on swarming cyber-physical systems (swarming CPS) consisting of a collection of mobile networked agents, each of which has sensing, computing, communication, and locomotion capabilities, and that have a wide range of civilian and military applications. Different from conventional static CPS, swarming CPS rely on mobile computing entities, e.g., robots, which collaboratively interact with phenomena of interest at different physical locations. This unique feature calls for novel sensing-motion co-design solutions to accomplish a variety of increasingly complex missions. Towards this, the overall research objective of this project is to establish and demonstrate a generic motion-sensing co-design procedure that will significantly reduce the complexity of the mission design for swarming CPS, and greatly facilitate the development of effective, efficient and adaptive control and sensing strategies under various environment uncertainties. This project aims to offer comprehensive scientific understanding of the dynamic nature of swarming CPS, contribute to generic engineering principles for designing collaborative control and sensing algorithms, and advance the enabling technologies of practically applying CPS in the challenging environment. The research solutions of this project aim to bring significant advance in the environmental sustainability, homeland security, and human well-being. The project provides unique interdisciplinary training opportunities for graduate and undergraduate students through both research work and related courses that the PIs will develop and offer. The project significantly advances the state of the art in cooperative control and sensing and provide an enabling technology for swarming CPS through highly interrelated thrusts: (1) a generic sensing and motion co-design procedure, which reveals the fundamental interplay between the sensing dynamics and motion dynamics of swarming CPS, will be proposed to facilitate the development of effective and efficient control and sensing strategies; (2) by following such co-design procedure, provable correct, computation efficient, and communication light control and sensing strategies will be developed for swarming CPS with constrained resources to accomplish specific missions, e.g., locating pollutants, in an unknown field, while navigating through uncertain spaces; (3) to provide an enabling mobile platform to verify the proposed strategies, innovative small, highly 3D maneuverable, noiseless, energy-efficient, and robust robotic fish fully actuated by smart material will be designed to meet the maneuvering requirements of the proposed algorithms; (4) novel Magnetic Induction (MI)-based underwater communication and localization solutions will be developed, which allows robotic fish to timely and reliably exchange messages, while simultaneously providing accurate inter-fish localization in the harsh 3D underwater environment; and (5) the proposed sensing-motion co-design strategies will be verified and demonstrated using a school of wirelessly interconnected robotic fish in both lab-based experiments and field experiments.

Recent developments in nanotechnology and synthetic biology have enabled a new direction in biological engineering: synthesis of collective behaviors and spatio-temporal patterns in multi-cellular bacterial and mammalian systems. This will have a dramatic impact in such areas as amorphous computing, nano-fabrication, and, in particular, tissue engineering, where patterns can be used to differentiate stem cells into tissues and organs. While recent technologies such as tissue- and organoid on-a-chip have the potential to produce a paradigm shift in tissue engineering and drug development, the synthesis of user-specified, emergent behaviors in cell populations is a key step to unlock this potential and remains a challenging, unsolved problem. This project brings together synthetic biology and micron-scale mobile robotics to define the basis of a next-generation cyber-physical system (CPS) called biological CPS (bioCPS). Synthetic gene circuits for decision making and local communication among the cells are automatically synthesized using a Bio-Design Automation (BDA) workflow. A Robot Assistant for Communication, Sensing, and Control in Cellular Networks (RA), which is designed and built as part of this project, is used to generate desired patterns in networks of engineered cells. In RA, the engineered cells interact with a set of micro-robots that implement control, sensing, and long-range communication strategies needed to achieve the desired global behavior. The micro-robots include both living and non-living matter (engineered cells attached to inorganic substrates that can be controlled using externally applied fields). This technology is applied to test the formation of various patterns in living cells. The project has a rich education and outreach plan, which includes nationwide activities for CPS education of high-school students, lab tours and competitions for high-school and undergraduate students, workshops, seminars, and courses for graduate students, as well as specific initiatives for under-represented groups. Central to the project is the development of theory and computational tools that will significantly advance that state of the art in CPS at large. A novel, formal methods approach is proposed for synthesis of emergent, global behaviors in large collections of locally interacting agents. In particular, a new logic whose formulas can be efficiently learned from quad-tree representations of partitioned images is developed. The quantitative semantics of the logic maps the synthesis of local control and communication protocols to an optimization problem. The project contributes to the nascent area of temporal logic inference by developing a machine learning method to learn temporal logic classifiers from large amounts of data. Novel abstraction and verification techniques for stochastic dynamical systems are defined and used to verify the correctness of the gene circuits in the BDA workflow.

Stroke is the leading cause of long-term disability in the US with approximately 7 million stroke survivors living in the US today and for patients with neurological disorders, it has been shown that limited gait velocity commonly results in walking that is predominantly restricted to the household. Unlike traditional exoskeletons which contain rigid linkage elements, the vision for this work is for exosuits that use soft materials such as textiles to provide a more conformal, unobtrusive and compliant means to interface to the human body. This represents a fundamental change in the paradigm of how people have viewed and designed wearable robots for the last half a century. Such a solution would have broad impact beyond the stroke patient population and could provide benefit to children with Cerebral Palsy or elderly individuals with muscle weakness. In addition there are plans to create a set of novel instructional educational toolkits for patient-in-the-loop cyber-physical systems that will be shared via an online portal and the CPS Virtual Organization (CPS-VO). With a patient-in-the-loop CPS, the patient, the physical suit, the computational control algorithms and the task/environment form a system in which all of the elements need to seamlessly interact. Through a modeling and experimental approach involving extensive human subjects studies, the team aims to create a unified engineering, biomechanical and physiological framework for designing and evaluating patient-in-the-loop CPS that include co-operative controllers that adapt in real-time to the patient to ensure safety and reliability an integrated system. Specifically the project will seek to gain a fundamental understanding of how to (1) analytically and experimentally characterize how forces are transmitted from these soft systems to the patient through the underlying soft tissue so as to generate assistance, (2) apply the optimal magnitude and timing of assistance to the patient to promote a more symmetric and natural gait by monitoring biomechanical, physiological and suit sensor data and (3) fuse information from different sensors monitoring patient motion and interaction forces to create an integrated CPS with a co-operative controller than can adapt to non-periodic movements of the patient.

The project focuses on swarming cyber-physical systems (swarming CPS) consisting of a collection of mobile networked agents, each of which has sensing, computing, communication, and locomotion capabilities, and that have a wide range of civilian and military applications. Different from conventional static CPS, swarming CPS rely on mobile computing entities, e.g., robots, which collaboratively interact with phenomena of interest at different physical locations. This unique feature calls for novel sensing-motion co-design solutions to accomplish a variety of increasingly complex missions. Towards this, the overall research objective of this project is to establish and demonstrate a generic motion-sensing co-design procedure that will significantly reduce the complexity of the mission design for swarming CPS, and greatly facilitate the development of effective, efficient and adaptive control and sensing strategies under various environment uncertainties. This project aims to offer comprehensive scientific understanding of the dynamic nature of swarming CPS, contribute to generic engineering principles for designing collaborative control and sensing algorithms, and advance the enabling technologies of practically applying CPS in the challenging environment. The research solutions of this project aim to bring significant advance in the environmental sustainability, homeland security, and human well-being. The project provides unique interdisciplinary training opportunities for graduate and undergraduate students through both research work and related courses that the PIs will develop and offer. The project significantly advances the state of the art in cooperative control and sensing and provide an enabling technology for swarming CPS through highly interrelated thrusts: (1) a generic sensing and motion co-design procedure, which reveals the fundamental interplay between the sensing dynamics and motion dynamics of swarming CPS, will be proposed to facilitate the development of effective and efficient control and sensing strategies; (2) by following such co-design procedure, provable correct, computation efficient, and communication light control and sensing strategies will be developed for swarming CPS with constrained resources to accomplish specific missions, e.g., locating pollutants, in an unknown field, while navigating through uncertain spaces; (3) to provide an enabling mobile platform to verify the proposed strategies, innovative small, highly 3D maneuverable, noiseless, energy-efficient, and robust robotic fish fully actuated by smart material will be designed to meet the maneuvering requirements of the proposed algorithms; (4) novel Magnetic Induction (MI)-based underwater communication and localization solutions will be developed, which allows robotic fish to timely and reliably exchange messages, while simultaneously providing accurate inter-fish localization in the harsh 3D underwater environment; and (5) the proposed sensing-motion co-design strategies will be verified and demonstrated using a school of wirelessly interconnected robotic fish in both lab-based experiments and field experiments.

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.

Driven by both civilian and military applications, such as coordinated surveillance, search and rescue, underwater or space exploration, manipulation in hazardous environments, and rapid emergency response, cooperative actions by teams of robots has emerged as an important research area. However, the coordination strategies for such robot teams are still developed to a great extent by trial-and-error processes. Hence, the strategies cannot guarantee mission success. This award supports fundamental research to provide a provably correct formal design theory of multi-robot systems that guarantees mission success. Furthermore, results from the research can be extended to the design of more general cyber-physical systems (CPSs) consisting of distributed and coordinated subsystems, such as the national power grid, ground/air traffic networks, and manufacturing systems. These CPSs are critical components of the national civil infrastructure that must operate reliably to ensure public safety. The multidisciplinary approach taken will help broaden participation of underrepresented groups in research and positively impact engineering education. Focusing on multi-robot teams, the goal of the research is to build foundations for a provably correct formal design theory for CPSs. This design theory will guarantee a given global performance of multi-robot teams through designing local coordination rules and control laws. The basic idea is to decompose the team mission into individual subtasks such that the design can be reduced to a local synthesis problem for individual robots. Multidisciplinary approaches combining hybrid systems, supervisory control, regular inference and model checking will be utilized to achieve this goal. The developed theory will enable robots in the team to cooperatively learn their individual roles in a mission, and then automatically synthesize local supervisors to fulfill their subtasks. A salient feature of this method lies on its ability to handle environmental uncertainties and unmodeled dynamics, as there is no need for an explicit model of the transition dynamics of each agent/robot and their interactions with the environment. In addition, the design is online and reactive, enabling the robot team to adapt to changing environments and dynamic tasking. The derived theory will be implemented as software tools and will be demonstrated through real robotic systems consisting of unmanned ground and aerial vehicles in unstructured urban/rural areas.

Driven by both civilian and military applications, such as coordinated surveillance, search and rescue, underwater or space exploration, manipulation in hazardous environments, and rapid emergency response, cooperative actions by teams of robots has emerged as an important research area. However, the coordination strategies for such robot teams are still developed to a great extent by trial-and-error processes. Hence, the strategies cannot guarantee mission success. This award supports fundamental research to provide a provably correct formal design theory of multi-robot systems that guarantees mission success. Furthermore, results from the research can be extended to the design of more general cyber-physical systems (CPSs) consisting of distributed and coordinated subsystems, such as the national power grid, ground/air traffic networks, and manufacturing systems. These CPSs are critical components of the national civil infrastructure that must operate reliably to ensure public safety. The multidisciplinary approach taken will help broaden participation of underrepresented groups in research and positively impact engineering education. Focusing on multi-robot teams, the goal of the research is to build foundations for a provably correct formal design theory for CPSs. This design theory will guarantee a given global performance of multi-robot teams through designing local coordination rules and control laws. The basic idea is to decompose the team mission into individual subtasks such that the design can be reduced to a local synthesis problem for individual robots. Multidisciplinary approaches combining hybrid systems, supervisory control, regular inference and model checking will be utilized to achieve this goal. The developed theory will enable robots in the team to cooperatively learn their individual roles in a mission, and then automatically synthesize local supervisors to fulfill their subtasks. A salient feature of this method lies on its ability to handle environmental uncertainties and unmodeled dynamics, as there is no need for an explicit model of the transition dynamics of each agent/robot and their interactions with the environment. In addition, the design is online and reactive, enabling the robot team to adapt to changing environments and dynamic tasking. The derived theory will be implemented as software tools and will be demonstrated through real robotic systems consisting of unmanned ground and aerial vehicles in unstructured urban/rural areas.

Designing software that can properly and safely interact with the physical world is an important cyber-physical systems design challenge. The proposed work includes the development of a novel approach to designing planning and control algorithms for high-performance cyber physical systems. The new approach was inspired by statistical mechanics and stochastic geometry. It will (i) identify behavior such as phase transitions in cyber-physical systems and (ii) capitalize this behavior in order to design practical algorithms with provable correctness and performance guarantees. The algorithms developed through this research effort hold the potential for immediate industrial impact, particularly in the development of real-time robotic systems. These algorithms may strengthen the rapidly developing U.S. robotics industry. The proposed research activity will also vitalize the PI?s educational plans. Undergraduate and graduate courses that make substantial contributions to the embedded systems education at MIT will be developed. The classes will focus on provably-correct controller synthesis for cyber-physical systems, which is currently not thought at MIT. Undergraduate students will be involved in research activities.

This INSPIRE award is partially funded by the Interdisciplinary Research Program in the Division of Civil, Mechanical and Manufacturing Innovation in the Directorate for Engineering, the Computer systems Research Program in the Division of Computer and Network Systems in the Directorate for Computer and Information Science and Engineering, and the Robust Intelligence Program in the Division of Information and Intelligent Systems in the Directorate for Computer and Information Science and Engineering. Integrated circuits are produced in billion-dollar chip fabs, which require many months of processing to go from a design to a chip. The goal of this proposal is to accomplish that in an afternoon, with a table-top process. Rather than etching or depositing electronic materials, as is done today, it is based on assembling digital materials. These use a discrete set of components, reversibly joined in a discrete set of relative positions and orientations. Those attributes allow positions to be determined by the parts, errors in their placement to be detected and corrected, dissimilar materials to be joined, and them to be disassembled rather than disposed. A conducting and insulating part type will be used to replace multilayer printed circuit boards, connectors and cabling for three-dimensional interconnect, inductors and capacitors, striplines and antennas. A resistive part type will be added for producing passive components, semiconducting part types will be added for active components, and magnetic and flexural part types for electromechanical components. This project will develop prototypes of the parts, the processes to produce them, the assemblers to place them, and the software tools to design with them. The research will progress in stages of size and complexity, reproducing the history of integrated electronics. First will be the equivalent of small-scale integration, using tens of parts with a 100 micron feature size. A test case at this level of integration will be assembling a radiofrequency matching network. Then will come medium-scale integration, using hundreds of parts with a 10 micron feature size. A goal here will be assembling a ring oscillator and binary counter. Finally, large-scale integration will use thousands of parts with a 1 micron feature size, with a goal of assembling a microprocessor. Computer-controlled manufacturing has progressed from subtractive to additive processes; this research roadmap will introduce the discrete assembly and disassembly of functional digital materials, to code the construction of complete systems in an integrated process.