Implantable Cardiac Defibrillators (ICDs) are at the forefront of preventing sudden death in patients suffering from ventricular arrhythmias. ICDs have evolved into complex Cyber-Physical Systems (CPS)which tightly sensing, hardware, and software to diagnose arrythmias based on electrogram signals and control cardiac excitation. These devices are life-critical, yet the Verification and Validation (V&V) techniques used for establishing their safety have remained somewhat informal, and rely largely on extensive unit testing. There have been a number of exciting developments in formal verification technologies. This proposal introduces these techniques into the ICD verification process, and will demonstrate their suitability for application in other medical devices. The project will develop a model-based framework for ICDs, and will apply formal verification techniques, such as model checking and reachability analysis, to high-fidelity cardiac electrophysiological models that capture the electrical excitation induced by the ICD's control software. Through extensive collaboration with FDA research staff, the proposal will demonstrate the effectiveness of formal verification technology and suitability in medical device applications.

Trustworthy operation of next-generation complex power grid critical infrastructures requires mathematical and practical verification solutions to guarantee the correct infrastructural functionalities. This project develops the foundations of theoretical modeling, synthesis and real-world deployment of a formal and scalable controller code verifier for programmable logic controllers (PLCs) in cyber-physical settings. PLCs are widely used for control automation in industrial control systems. A PLC is typically connected to an engineering workstation where engineers develop the control logic to process the input values from sensors and issue control commands to actuators. The project focuses on protecting infrastructures against malicious control injection attacks on PLCs, such as Stuxnet, that inject malicious code on the device to drive the underlying physical platform to an unsafe state. The broader impact of this proposal is highly significant. It offers potential for real-time security for critical infrastructure systems covering sectors such as energy and manufacturing. The project's intellectual merit is in providing a mathematical and practical verification framework for cyber-physical systems through integration of offline formal methods, online monitoring solutions, and power systems analysis. Offline formal methods do not scale for large-scale platforms due to their exhaustive safety analysis of all possible system states, while online monitoring often reports findings too late for preventative action. This project takes a hybrid approach that dynamically predicts the possible next security incidents and reports to operators before an unsafe state is encountered, allowing time for response. The broader impact of this project is in providing practical mathematical analysis capabilities for general cyber-physical safety-critical infrastructure with potential direct impact on our national security. The research outcomes are integrated into education modules for graduate, undergraduate, and K-12 classrooms.

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.

This project develops a theoretical framework as well as software tools to support testing and verification of a Cyber-Physical System (CPS) within a Model-Based Design (MBD) process. The theoretical bases of the framework are stochastic optimization methods, and robustness notions of formal specification languages. The project's research comprises three components: development of conditions on the algorithms and on the structure of the CPS for inferring finite-time guarantees on the randomized testing process; the study of testing methods that can support modular and compositional system design; and investigation of appropriate notions of conformance between two system models and between a model and its implementation on a computational platform. All of these components are needed to support testing and verification in all the stages of an MBD process as well as to support component reuse, incremental system improvements and modular design. The evaluation of the framework is driven by the problems of verifying automotive control systems and medical devices. As safety-critical CPS become ubiquitous, the need for design methods that guarantee correct system functionality and performance becomes more urgent. Certification and government agencies need dependable testing and verification tools to incorporate in certification standards and procedures. The concrete benefits to the society are both in terms of reduced catastrophic design errors in new products and in terms of reduced economic costs for new product development. The former increases the confidence in new technologies while the latter improves the competitiveness of the companies that utilize such technologies. The theoretical results of this project are being incorporated into software tools for testing, verification and validation of complex CPS. The evaluation focus of the project on verifying infusion pumps and automotive control software ultimately helps in avoiding harmful losses due to errors in these safety-critical systems. The use of any software tool that is based on formal or semi-formal methods requires engineers with solid training on these technologies. This proposal puts forward an education curriculum for developing new courses that introduce formal and semi-formal methods for CPS at all levels of higher education, i.e., undergraduate, graduate and continuing education. Particular attention is devoted into on-line continuing education of practicing engineers who must acquire new MBD skills.

This project aims to achieve key technology, infrastructure, and regulatory science advances for next generation medical systems based on the concept of medical application platforms (MAPs). A MAP is a safety/security-critical real-time computing platform for: (a) integrating heterogeneous devices and medical IT systems, (b) hosting application programs ("apps") that provide medical utility through the ability to both acquire information and update/control integrated devices, IT systems, and displays. The project will develop formal architectural and behavioral specification languages for defining MAPs, with a focus on techniques that enable compositional reasoning about MAP component interoperability and safety. These formal languages will include an extensible property language to enable the specification of real-time, quality-of-service, and attributes specific to medical contexts that can be leveraged by code generation, testing, and verification tools. The project will work closely with a synergistic team of clinicians, device industry partners, regulators, and medical device interoperability and safety standard organizations to develop an open source MAP innovation platform to enable key stakeholders within the nation's health care ecosphere to identify, prototype, and evaluate solutions to key technology and regulatory challenges that must be overcome to develop a commodity market of regulated MAP components. Because MAPs provide pre-built certified infrastructure and building blocks for rapidly developing multi-device medical applications, this research has the potential to usher in a new paradigm of medical system that significantly increases the pace of innovation, lowers development costs, enables new functionality by aggregating multiple devices into a system of systems, and achieves greater system safety.

The objective of this project is to create a focused cyber-physical design environment to accelerate the development of miniature medical devices in general and swallowable systems in particular. The project develops new models and tools including a web-based integrated simulation environment,capturing the interacting dynamics of the computational and physical components of devices designed to work inside the human body, to enable wider design space exploration, and, ultimately, to lower the barriers which have thus far impeded system engineering of miniature medical devices. Currently, a few select individuals with deep domain expertise create these systems. The goal is to open this field to a wider community and at the same time create better designs through advanced tool support. The project defines a component model and corresponding domain-specific modeling language to provide a common framework for design capture, design space exploration, analysis and automated synthesis of all hardware and software artifacts. The project also develops a rich and extensible component and design template library that designers can reuse. The online design environment will provide early feedback and hence, it will lower the cost of experimentation with alternatives. The potential benefit is not just incremental (in time and cost), but can lead to novel ideas by mitigating the risk of trying unconventional solutions. Trends in consumer electronics such as miniaturization, low power operation, and wireless technologies have enabled the design of miniature devices that hold the potential to revolutionize medicine. Transformational societal public health benefits (e.g., early diagnosis of colorectal cancer or prevention of heart failure) are possible through less invasive and more accurate diagnostic and interventional devices. By eliminating large incisions in favor of natural orifices or small ports, these medical devices can increase diagnostic screening effectiveness and reduce pain and recovery time. Furthermore, if successful, the proposed scientific approach can be extended to any other application, wherever size, power efficiency, and high confidence are stringent requirements. The educational plan of the project is centered on the web-based design environment that will also contain an interface for high school students to experiment with medical cyber-physical devices in a virtual environment. Students will be able to build medical devices from a library of components, program them using an intuitive visual programming language and operate them in various simulated environments. A Summer Camp organized in the framework of this project will enhance students learning experience with real hands-on experimentation in a lab.

Wireless body area sensing networks (WBANs) have the potential to revolutionize health care in the near term and enhance other application domains including sports, entertainment, military and emergency situations. These WBANs represent a novel cyber-physical system that unites engineering systems, the natural world and human individuals. The coupling of bio-sensors with a wireless infrastructure enables the real-time monitoring of an individual's health, environment and related behaviors continuously, as well as the provision of real-time feedback with nimble, adaptive, and personalized interventions. Recent technological advances in low power integrated circuits, signal processing and wireless communications have enabled the design of tiny, low cost, lightweight, intelligent medical devices, sensors and networking platforms that have the potential to make the concept of truly pervasive wireless sensor networks a reality. To develop the WBANs of the future, this breakthrough research will pursue the interfaces of sensing, communication and control. This project aims to investigate energy and delay sensitive sensing, communication, decision-making and control for health monitoring application of wireless body area networks. In these systems, sensors with varying accuracy observe heterogeneous source signals that must be processed and communicated and used for inference and decision-making purposes. All of these operations must be carried out in the presence of constraints on power and energy resources at the sensors, limited communication and computational abilities and with low end-to-end delay between the sensing of information to its eventual utilization. In this project, a global (end-to end) perspective is adopted that optimizes network operation to improve the information quality and enhance the lifetime of the network, focusing in particular on optimal use of sensor resources such as energy, new sensing and communication paradigms that balance information quality and energy expenditure, and real-time encoding and decoding methods that provide strict delay guarantees on information delivery. The proposed work will contribute to several research areas including optimal resource allocation at sensors, adaptive sensing methods, real-time encoding and decoding and event-based communication. The educational impact of the proposed research will come through the training of new information technology professionals and scientists with expertise in cross-disciplinary research, development of new courses based on the proposed research activity and continued efforts to include women and under-represented minorities in the research program.

Buildings in the U.S. contribute to 39% of energy use, consume approximately 70% of the electricity, and account for 39% of CO2 emissions. Hence, developing green building architectures is an extremely critical component in energy sustainability. The investigators will develop a unified analytical approach for green building design that comprehensively manages energy sustainability by taking into account the complex interactions between these systems of systems, providing a high degree of security, agility and robust to extreme events. The project will serve to advance the general science in CPS, help bridge the gap between the cyber and civil infrastructure communities, educate students across different disciplines, include topics in curriculum development, and actively recruit underrepresented minority and undergraduate students. The main thesis of this research is that ad hoc green energy designs are often myopic, not taking into account key interdependencies between subsystems and users, and thus often lead to undesirable solutions. In fact, studies have shown that 28%-35% of LEED-certified buildings consumed more energy than their conventional counterparts, all of which calls for the development of a comprehensive analytical foundation for designing green buildings. In particular, the investigators will focus on three interrelated thrust areas: (i) Integrated energy management for a single-building, where the goal is to jointly consider the complex interactions among building subsystems. The investigators will develop novel control schemes that opportunistically exploit the energy demand elasticity of the building subsystems and adapt to occupancy patterns, human comfort zones, and ambient environments. (ii) Managing multi-building interactions to develop (near) optimal distributed control and coordination schemes that provide performance guarantees. (iii) Designing for anomalous conditions such as extreme weather and malicious attacks, where power grid connections and/or cyber-networks are disrupted. The research will provide directions at developing an analytical foundation and cross-cutting principles that will shed insight on the design and control of not only building systems, but also general CPS systems. An important goal is to help bridge the gap between the networking, controls, and civil infrastructure communities by giving talks and publishing works in all of these forums. The investigators will disseminate the research findings to industry as well as offer education and outreach programs to the K-12 students in STEM disciplines. The investigators will also actively continue their already strong existing efforts in recruiting women and underrepresented minorities, as well as providing rich research experience to undergraduate REU students. This project will provide fertile training for students spanning civil infrastructure research, networking, controls, optimization, and algorithmic development. The investigators will also actively include the outcomes of the research in existing and new courses at both the Ohio State University and Virginia Tech.

The objective of this research is an injection of new modeling techniques into the area of Cyber-Physical Systems (CPSs). The approach is to design new architectures for domain-specific modeling tools in order to permit feedback from analysis, validation, and verification engines to influence how CPSs are designed. This project involves new research into the integration of existing, heterogeneous modeling languages in order to address problems in CPS design, rather than a single language for all CPS. Since many tools for analysis, validation, and verification focus on at most two of the three major components of CPS (communication, computation, and control), new paradigms in modeling are used to integrate tools early in the design process. The algorithms and software developed in this project run validation and verification tools on models, and then close the loop by using the tool outputs to automatically modify the system models. The satisfaction of design requirements in CPSs is critical for tomorrow's societal technologies such as smart buildings, home healthcare, and water management. Among the most compelling design requirements are those of safety, and CPSs for autonomous vehicles exemplify this well. By involving a full-sized autonomous vehicle in this project, the validation and verification of safety requirements is tied to a concrete platform that is broadly understood. By involving students in the design of behaviors of the vehicle, the project exposes scientists and engineers of tomorrow to societal-scale problems, and tools to address them.

This project will improve the communication, teaching and leadership skills of graduate students conducting research in Cyber-Physical Systems (CPS) via teaching and mentoring in 7-12 secondary education, while advancing their research through the planned inquiry-based educational activities. The graduate fellows selected from multidisciplinary engineering disciplines will partner with teachers in planning, preparing and delivering CPS related enhancements to existing science and technology course topics, hence infusing CPS related basic engineering concepts into grades 7-12. Fellows will partner with selected teachers of technology, science, and math, and will act as role models and in-class ?resource persons?, while also mentoring students in various engineering and computational aspects of Alaska relevant CPS applications and projects. The educational activities and projects will be directly related to the fellows? CPS research, such as autonomous unmanned ground and aerial vehicles for exploration and search & rescue in the Arctic, internet-based bilateral control and teleoperation systems; sensor/actuator networks for decision support systems and for energy efficient automated buildings. CYBER-Alaska will address this need and provide systematic mentorship for engineering education with different applications of CPS, a theme identified as the technology of 21st century and a top priority for the USA. Our project will contribute to the education and training of well-rounded graduate students in this emerging area, while also addressing the urgent technical educational needs of Alaska public teachers and students, primarily aiming for rural schools and schools with high percentage of minorities and Alaskan natives.