All cyber-physical systems (CPS) depend on properly calibrated sensors to sense the surrounding environment. Unfortunately, the current state of the art is that calibration is often a manual and expensive operation; moreover, many types of sensors, especially economical ones, must be recalibrated often. This is typically costly, performed in a lab environment, requiring that sensors be removed from service. MetaSense will reduce the cost and management burden of calibrating sensors. The basic idea is that if two sensors are co-located, then they should report similar values; if they do not, the least-recently-calibrated sensor is suspect. Building on this idea, this project will provide an autonomous system and a set of algorithms that will automate the detection of calibration issues and preform recalibration of sensors in the field, removing the need to take sensors offline and send them to a laboratory for calibration. The outcome of this project will transform the way sensors are engineered and deployed, increasing the scale of sensor network deployment. This in turn will increase the availability of environmental data for research, medical, personal, and business use. MetaSense researchers will leverage this new data to provide early warning for factors that could negatively affect health. In addition, graduate student engagement in the research will help to maintain the STEM pipeline. This project will leverage large networks of mobile sensors connected to the cloud. The cloud will enable using large data repositories and computational power to cross-reference data from different sensors and detect loss of calibration. The theory of calibration will go beyond classical models for computation and physics of CPS. The project will combine big data, machine learning, and analysis of the physics of sensors to calculate two factors that will be used in the calibration. First, MetaSense researchers will identify measurement transformations that, applied in software after the data collection, will generate calibrated results. Second, the researchers will compute the input for an on-board signal-conditioning circuit that will enable improving the sensitivity of the physical measurement. The project will contribute research results in multiple disciplines. In the field of software engineering, the project will contribute a new theory of service reconfiguration that will support new architecture and workflow languages. New technologies are needed because the recalibration will happen when the machine learning algorithms discover calibration errors, after the data has already been collected and processed. These technologies will support modifying not only the raw data in the database by applying new calibration corrections, but also the results of calculations that used the data. In the field of machine learning, the project will provide new algorithms for dealing with spatiotemporal maps of noisy sensor readings. In particular, the algorithms will work with Gaussian processes and the results of the research will provide more meaningful confidence intervals for these processes, substantially increasing the effectiveness of MetaSense models compared to the current state of the art. In the field of pervasive computing, the project will build on the existing techniques for context-aware sensing to increase the amount of information available to the machine learning algorithms for inferring calibration parameters. Adding information about the sensing context is paramount to achieve correct calibration results. For example, a sensor that measures air pollution inside a car on a highway will get very different readings if the car window is open or closed. Finally, the project will contribute innovations in sensor calibration hardware. Here, the project will contribute innovative signal-conditioning circuits that will interact with the cloud system and receive remote calibration parameters identified by the machine learning algorithms. This will be a substantial advance over current circuits based on simple feedback loops because it will have to account for the cloud and machine learning algorithms in the loop and will have to perform this more complex calibration with power and bandwidth constraints. Inclusion of graduate students in the research helps to maintain the STEM pipeline.

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.

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.

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.

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.