Errors in cyber-physical systems can lead to disastrous consequences. Classic examples date back to the Therac-25 radiation incidents in 1987 and the Ariane 5 rocket crash in 1996. More recently, Toyota's unintended acceleration bug was caused by software errors, and certain cars were found vulnerable to attacks that can take over key parts of the control software, allowing attackers to even disable the brakes remotely. Pacemakers have also been found vulnerable to attacks that can cause deadly consequences for the patient. To reduce the chances of such errors happening, this project investigates the application of a technique called Foundational Verification to cyber-physical systems. In Foundational Verification, the system being developed is proved correct, in full formal detail, using a proof assistant. The main intellectual merit of the proposal is the attainment of previously unattainable levels of safety for cyber-physical systems because proofs in Foundational Verification are carried out in complete detail. To ensure that the techniques in this project are practical, they are evaluated within the context of a real flying quadcopter. The project's broader significance and importance is the improved correctness, safety and security of cyber-physical systems. In particular, this project lays the foundation for ushering in a new level of formal correctness for cyber-physical systems. Although the initial work focuses on quadcopters, the concepts, ideas, and research contributions have the potential for transformative impact on other kinds of systems, including power-grid software, cars, avionics and medical devices (from pacemakers and insulin pumps to defibrillators and radiation machines).

Cells, to carry out many important functions, employ an elaborate transport network with bio-molecular components forming roadways as well as vehicles. The transport is achieved with remarkable robustness under a very uncertain environment. The main goal of this proposal is to understand how biology achieves such functionality and leveraging the knowledge toward realizing effective engineered transport mechanisms for micron sized cargo. The realization of a robust infrastructure that enables simultaneous transport of many micron and smaller sized particles will have a transformative impact on a vast range of areas such as medicine, drug development, electronics, and bio-materials. A key challenge here is to probe the mechanisms often at the nanometer scale as the bio-molecular components are at tens of nanometer scale. The main tools for addressing these challenges come from an engineering perspective that is guided by existing insights from biology. The proposal will bring together researchers from engineering and biology and it provides an integrated environment for students. Moreover, it is known that an impaired transport mechanism can underlie many neurodegenerative maladies, and as the research here pertains to studying intracellular transport, discoveries hold the potential for shedding light on what causes the impaired transport. Robust infrastructure that enables simultaneous transport of many micron and smaller sized particles will have a transformative impact on a vast range of areas such as medicine, drug development, electronics, and bio-materials. Daunting challenges from the underlying highly uncertain and complex environments impede enabling robust and efficient transport systems at micro-scale. Motivated by transport in biological cells, this work proposes a robust and efficient engineered infrastructure for transporting micron/molecular scale cargo using biological constructs. For probing and manipulating the transport network, the proposal envisions strategies for coarse and fine resolution objectives at the global and local scales respectively. At the fine scale of monitoring and control, scarce and expensive physical resources such as high resolution sensors have to be shared for interrogation/control of multiple carriers. In this proposal, the principles for joint control, sensor allocation and scheduling of resources to achieve enhanced performance objectives of a high resolution probing tool, will be developed. A modern control perspective forms an essential strategy for managing multiple objectives. At the global scale, entire traffic will be monitored to arrive at real-time and off-line inferences on traffic modalities. Associated principles for dynamically identifying and tracking clusters of carriers and their importance will be built. This categorization of physical elements and their importance will determine the dynamic allocation of computational resources. Associated study of trade-offs will guide a combined strategy for allocation of computational resources and gathering of information on physical elements. Methods based on the reconstruction of graph topologies for reaching inferences that are suited to dynamically related time trajectories for the transportation infrastructure will be developed. The research proposed is transformative as it will enable a new transport paradigm at the cellular scale, which will also provide unique insights into intracellular transport where it will be possible to investigate multiple factors under the same experimental conditions.

Assistive machines - like powered wheelchairs, myoelectric prostheses and robotic arms - promote independence and ability in those with severe motor impairments. As the state- of-the-art in these assistive Cyber-Physical Systems (CPSs) advances, more dexterous and capable machines hold the promise to revolutionize ways in which those with motor impairments can interact within society and with their loved ones, and to care for themselves with independence. However, as these machines become more capable, they often also become more complex. Which raises the question: how to control this added complexity? A new paradigm is proposed for controlling complex assistive Cyber-Physical Systems (CPSs), like robotic arms mounted on wheelchairs, via simple low-dimensional control interfaces that are accessible to persons with severe motor impairments, like 2-D joysticks or 1-D Sip-N-Puff interfaces. Traditional interfaces cover only a portion of the control space, and during teleoperation it is necessary to switch between different control modes to access the full control space. Robotics automation may be leveraged to anticipate when to switch between different control modes. This approach is a departure from the majority of control sharing approaches within assistive domains, which either partition the control space and allocate different portions to the robot and human, or augment the human's control signals to bridge the dimensionality gap. How to best share control within assistive domains remains an open question, and an appealing characteristic of this approach is that the user is kept maximally in control since their signals are not altered or augmented. The public health impact is significant, by increasing the independence of those with severe motor impairments and/or paralysis. Multiple efforts will facilitate large-scale deployment of our results, including a collaboration with Kinova, a manufacturer of assistive robotic arms, and a partnership with Rehabilitation Institute of Chicago. The proposal introduces a formalism for assistive mode-switching that is grounded in hybrid dynamical systems theory, and aims to ease the burden of teleoperating high-dimensional assistive robots. By modeling this CPS as a hybrid dynamical system, assistance can be modeled as optimization over a desired cost function. The system's uncertainty over the user's goals can be modeled via a Partially Observable Markov Decision Processes. This model provides the natural scaffolding for learning user preferences. Through user studies, this project aims to address the following research questions: (Q1) Expense: How expensive is mode-switching? (Q2) Customization Need: Do we need to learn mode-switching from specific users? (Q3) Learning Assistance: How can we learn mode-switching paradigms from a user? (Q4) Goal Uncertainty: How should the assistance act under goal uncertainty? How will users respond? The proposal leverages the teams shared expertise in manipulation, algorithm development, and deploying real-world robotic systems. The proposal also leverages the teams complementary strengths on deploying advanced manipulation platforms, robotic motion planning and manipulation, and human-robot comanipulation, and on robot learning from human demonstration, control policy adaptation, and human rehabilitation. The proposed work targets the easier operation of robotic arms by severely paralyzed users. The need to control many degrees of freedom (DoF) gives rise to mode-switching during teleoperation. The switching itself can be cumbersome even with 2- and 3-axis joysticks, and becomes prohibitively so with more limited (1-D) interfaces. Easing the operation of switching not only lowers this burden on those already able to operate robotic arms, but may open use to populations to whom assistive robotic arms are currently inaccessible. This work is clearly synergistic: at the intersection of robotic manipulation, human rehabilitation, control theory, machine learning, human-robot interaction and clinical studies. The project addresses the science of CPS by developing new models of the interaction dynamics between the system and the user, the technology of CPS by developing new interfaces and interaction modalities with strong theoretical foundations, and the engineering of CPS by deploying our algorithms on real robot hardware and extensive studies with able-bodied and users with sprinal cord injuries.

Children affected by neurological conditions (e.g., Cerebral Palsy, Muscular Atrophy, Spina Bifida and Severe head trauma) often develop significant disabilities including impaired motor control. In many cases, walking becomes a non-functional and exhausting skill that demands the use of the aids or the substitution of function, such as wheelchair. This usually cause these children not to acquire locomotion skills, and consequently to lose their independence. However, it is well understood that bipedal locomotion, an essential human characteristic, ensures the best physiological motor pattern acquisition. For this reason, in children with neurological and neuromuscular diseases, independent walking is a significant rehabilitation goal that must be pursued in a specific temporal window due to the plasticity of central nervous system. In other words, children with neurological conditions have a small window of time to acquire locomotion skills through assisted walking rehearsals. The objective of this research work is to create and experimentally validate a set of technologies that form the framework for the development of adaptive, self-balancing, and modular exoskeleton robotics systems for children with neurological disorders. It is our belief that the exoskeleton (and its associated infrastructure) resulting from this research will offer an effective tool to promote locomotion skill acquisition, and in general health, during a critical period in the early life of children with neurological conditions. This research proposal develops a data-driven human-machine modeling specific to physiological conditions. This creates regression models that predict the user behavior without explicit modeling the complex human musculoskeletal dynamics and motor control mechanism. Additionally this research project formulates a safe adaptive control problem as a model predictive control (MPC) problem. In this method, an optimal input sequence is computed by solving a constrained finite-time optimal control problem where exoskeleton intrusion (input from exoskeleton) is minimized to maximize the user's intent to promote learning. This project further develops a novel approach for stabilizing and preventing fall of the exoskeleton and the child as a whole. This method allows a child wearing an exoskeleton to learn locomotion skills described above with less likelihood of falls. This research project furthermore evaluates the developed technologies in terms of efficiency and efficacy and creates a novel fun game using exoskeleton for children to promote locomotion skills.