The objective of this research is to develop new models of computation for multi-robot systems. Algorithm execution proceeds in a cycle of communication, computation, and motion. Computation is inextricably linked to the physical configuration of the system. Current models cannot describe multi-robot systems at a level of abstraction that is both manageable and accurate. This project will combine ideas from distributed algorithms, computational geometry, and control theory to design new models for multi-robot systems that incorporate physical properties of the systems. The approach is to focus on the high-level problem of exploring an unknown environment while performing designated tasks, and the sub-problem of maintaining network connectivity. Key issues to be studied will include algorithmic techniques for handling ongoing discrete failures, and ways of understanding system capabilities as related to failure rates, geometric assumptions and physical parameters such as robot mobility and communication bandwidth. New metrics will be developed for error rates and robot mobility. Intellectual merit arises from the combination of techniques from distributed algorithms, computational geometry, and control theory to develop and analyze algorithms for multi-robot systems. The project will develop a new class of algorithms and techniques for their rigorous analysis, not only under ideal conditions, but under a variety of error assumptions. The project will test theoretical ideas empirically, on three different multi-robot systems. Broader impacts will include new algorithms for robot coordination, and rigorous understanding of the capabilities of different hardware platforms. Robots are an excellent outreach tool, and provide concrete examples of theory in action.

The objective of this research is to check correct functioning of cyber-physical systems during their operation. The approach is to continuously monitor the system and raise an alarm when the system seems to exhibit an erroneous behavior. Correct functioning of cyber-physical systems is of critical importance. This is more so in safety critical systems like medical, automotive and other applications. The approach employs hybrid automata for specifying the property to be monitored and for modeling the system behavior. The system behavior is probabilistic in nature due to noise and other factors. Monitoring such systems is challenging since the monitor can only observe system outputs, but not it's state. Fundamental research, on defining and detecting whether a system is monitorable, is the focus of the work. The project proposes accuracy measures and cost based metrics for optimal monitoring. The project is developing efficient and effective monitoring techniques, based on product automata and Partially Observable Markov Decision Processes. The results of the project are expected to be transformative in ensuring correct operation of systems. The results will have impact in many areas of societal importance and utility for daily life, such as health care, nursing/rehabilitation, automotive systems, home appliances, and more. The benefits in nursing/rehabilitation emanate from the deployment of advanced technologies to assist caregivers. This can lead to improved health and quality of life of older patients at reduced costs. The project includes education and outreach in the form of K-12 outreach and involvement of undergraduate and graduate students in research. The project is committed to involving women and minorities in education and research.

The objective of this research is to establish a foundational framework for smart grids that enables significant penetration of renewable DERs and facilitates flexible deployments of plug-and-play applications, similar to the way users connect to the Internet. The approach is to view the overall grid management as an adaptive optimizer to iteratively solve a system-wide optimization problem, where networked sensing, control and verification carry out distributed computation tasks to achieve reliability at all levels, particularly component-level, system-level, and application level. Intellectual merit. Under the common theme of reliability guarantees, distributed monitoring and inference algorithms will be developed to perform fault diagnosis and operate resiliently against all hazards. To attain high reliability, a trustworthy middleware will be used to shield the grid system design from the complexities of the underlying software world while providing services to grid applications through message passing and transactions. Further, selective load/generation control using Automatic Generation Control, based on multi-scale state estimation for energy supply and demand, will be carried out to guarantee that the load and generation in the system remain balanced. Broader impact. The envisioned architecture of the smart grid is an outstanding example of the CPS technology. Built on this critical application study, this collaborative effort will pursue a CPS architecture that enables embedding intelligent computation, communication and control mechanisms into physical systems with active and reconfigurable components. Close collaborations between this team and major EMS and SCADA vendors will pave the path for technology transfer via proof-of-concept demonstrations.

The objective of this research is to develop formal verification tools for human-computer interfaces to cyber-physical systems. The approach is incorporating realistic assumptions about the behavior of humans into the verification process through mathematically constructed "mistake models" for common types of mistakes committed by the operator during an interactive task. Exhaustive verification techniques are used to expose combinations of human mistakes that can lead to system-wide failures. The techniques are evaluated using case studies involving medical device interfaces. The problem of verifying human-machine interfaces requires new approaches that combine rigorous formal verification techniques with the empirical human-centered approach to user-interface evaluation. The research addresses challenges of integrating empirical user-study data into formal game-based models that describe common types of operator mistakes. Using these models to detect subtle flaws in user-interface design is also a challenge. It is well-known that a poorly designed interface will enable harmful operator errors, which remain a major cause of failures in a wide variety of safety-critical cyber-physical systems. This project will automate user-interface verification by detecting likely defects, early in the design process. Open source verification tools will be made freely available to the community at large. The ongoing research will be integrated into a set of graduate-level computer science courses focused on the theme of "Safety in Human Computer Interfaces". Results from the project will also be integrated into educational materials for the ongoing eCSite GK12 project with the goal of promoting awareness of user-interface design issues amongst high school students.

The objective of this research is to develop new methods for verifying the safety of complex cyber-physical systems based on information derived from the wide variety of models and methods used throughout the design process. The approach is based on a new formalism to represent the architecture of systems with cyber components, physical components, and interconnections between these domains. Diverse engineering models of different aspects of the system will be associated through the cyber-physical architecture for the complete system. Formal logic will be developed to express and reason about inter-model consistency and to infer system-level properties from information derived from the domain-specific models. The project's intellectual merit lies in the creation of a comprehensive, unified framework for verifying properties of systems rich in both cyber and physical components. The new formal logic will make it possible to integrate information from the wide range of engineering domains and technical expertise required to design complex systems. This will lead to a principled, rigorous approach to system-level verification engineering for real-world cyber-physical systems. The application of the new methodology to verify the safety of cooperative intersection collision avoidance systems will have immediate impact on emerging technologies for safer automobile systems. A new interdisciplinary course in engineering and computer science on system-level design of cyber-physical systems will prepare a new cadre of graduates with the cross-cutting skills needed to develop safety-critical systems. Innovative educational modules will also be developed to inspire pre-college students to pursue education and careers in engineering and computer science.

The objective of this research is to develop a new approach for composition of safety-critical cyber-physical systems from a small code base of verified components and a large code base of unverified commercial off-the-shelf components. The approach is novel in that it does not require generating the entire code base from formal languages, specifications, or models and does not require verification to be applied to all code. Instead, an explicit goal is to accommodate large amounts of legacy code that is typically too complex to verify. The project introduces a set of verified component wrappers around existing unverified code, such that specified global system properties hold. The intellectual merit of the project lies in its innovative approach for managing component interactions. Unexpected interactions are the primary source of failure in cyber-physical systems. A fundamental conceptual challenge is to understand the different interaction spaces of cyber-physical system components and determine a set of trigger conditions when certain interactions must be restricted to prevent failure. The project develops analysis techniques that help understand the different interaction types and provides component wrappers to restrict them when necessary. Broader impact lies in significantly reducing the design and composition effort for the next generation of safety-critical embedded systems. A variety of student projects are being offered to undergraduates and graduate students. The researchers especially encourage women and minorities to participate. Outreach activity, such as hosting K-12 students on school field/science days, further strengthen the educational component. Technology transfer to John Deere is expected.

The objective of this research is to establish a new development paradigm that enables the effective design, implementation, and certification of medical device cyber-physical systems. The approach is to pursue the following research directions: 1) to support medical device interconnectivity and interoperability with network-enabled control; 2) to apply coordination between medical devices to support emerging clinical scenarios; 3) to ?close the loop? and enable feedback about the condition of the patient to the devices delivering therapy; and 4) to assure safety and effectiveness of interoperating medical devices. The intellectual merits of the project are 1) foundations for rigorous development, which include formalization of clinical scenarios, operational procedures, and architectures of medical device systems, as well as patient and caregiver modeling; 2) high-confidence software development for medical device systems that includes the safe and effective composition of clinical scenarios and devices into a dynamically assembled system; 3) validation and certification of medical device cyber-physical systems; and 4) education of the next-generation of medical device system developers who must be literate in both computational and physical aspects of devices. The broader impacts of the project will be achieved in three ways. Novel design methods and certification techniques will significantly improve patient safety. The introduction of closed-loop scenarios into clinical practice will reduce the burden that caregivers are currently facing and will have the potential of reducing the overall costs of health care. Finally, the educational efforts and outreach activities will increase awareness of careers in the area of medical device systems and help attract women and under-represented minorities to the field.

The objective of this research is to develop methods and tools for designing, implementing and verifying medical robotics. The approach is to capture the computational work-flow of systems with cyber, physical and biological components, to verify that work-flow and to synthesize systems from the work-flow model. The focusing application of this research is MRI-guided, high-frequency ultrasonic tumor ablation. MRI-guided ultrasonic tumor ablation poses challenges beyond the scope of current verification techniques. Medicine is filled with highly non-linear biological systems, which puts them at the frontier of mathematically rigorous correctness checking and verification. For instance, in this research, guaranteeing the safety of a cancer patient undergoing treatment will require verifying against Pennes bioheat equation, a non-linear differential equation with dozens of environmental factors. This research tackles such complexity using tiers of abstractions to efficiently, precisely and safely approximate the behavior of each component of a system. To ensure a faithful implementation of controllers, this research will investigate synthesizing the control code directly from the verified model in a correct by construction manner. The project will help develop the most appropriate family of formal methods for handling the safety and correctness challenges in the area of medical robotics. It directly addresses the CPS agenda of methods and tools by proposing formal techniques that bridge the gap between the cyber and physical elements. It will train manpower in cross-disciplinary areas through new seminars, workshops and courses. And, last but not least, the project will make a direct humanitarian impact on the well-being of society.

Complex surgical procedures in hospitals are increasingly aided by robotic surgery systems, often at the request of patients. These systems allow greatly increased precision, reach and flexibility to the surgeon. However, their powerful capabilities entail substantial system complexity in both hardware and software. The high probability of serious injuries should a malfunction occur calls for rigorous assessment and monitoring of the reliability and safety of these cyber-physical systems. In this research project, a framework for assessing and monitoring the reliability and safety of robotic surgery systems during development, field testing, and general deployment is being developed. The proposed framework complements existing techniques used in earlier phases of validation by taking into account how surgeons actually use a robotic surgery system, how it is affected by operating conditions, and how its observable behavior is related to its hardware and software dynamics. Before deployment, this framework uses accurate simulations to assess pre-clinical reliability. After deployment, the framework uses data collection through online monitoring of the system as it is being used in the field, followed by analysis to obtain assessments of operational reliability and safety. The collected data is also used to improve the simulations for future testing. The framework also aims to support post-market surveillance of these systems by providing a workable basis for reassessing reliability and safety properties after system maintenance. The developed tools and methods will also have applications in the validation of safety and reliability of other medical devices with embedded software and other cyber-physical systems in general.