The CrAVES project seeks to lay down intellectual foundations for credible autocoding of embedded systems, by which graphical control system specifications that satisfy given open-loop and closed-loop properties are automatically transformed into source code guaranteed to satisfy the same properties. The goal is that the correctness of these codes can be easily and independently verified by dedicated proof checking systems. During the autocoding process, the properties of control system specifications are transformed into proven assertions explicitly written in the resulting source code. Thus CrAVES aims at transforming the extensive safety and reliability analyses conducted by control system engineers, such as those based on Lyapunov theory, into rigorous, embedded analyses of the corresponding software implementations. CrAVES comes as a useful complement to current static software analysis methods, which it leverages to develop independent verification systems. Computers and computer programs used to manage documents and spreadsheets. They now also interact with physical artifacts (airplanes, power plants, automobile brakes and robotic surgeons), to create Cyber-Physical Systems. Software means complexity and bugs - bugs which can cause real tragedy, far beyond the frozen screens we associate with system crashes on our current PCs. Software autocoding is becoming the de facto recommended practice for many safety-critical applications. CrAVES aims to evolve this towards higher standards of quality and reduced design times and costs. Rigorous, mathematical arguments supporting safety-critical functionalities are the cornerstone of CrAVES. Collaborative programs involving high-school teachers will encourage the transmission of this message to STEM education in high-schools through university programs designed for that purpose.

Holonic Multi-Agent Control of Intelligent Power Distribution Systems This project will demonstrate a Holonic Multiagent System Architecture capable of adaptively controlling future electrical power distribution systems (PDS), which are expected to include a large number of renewable power generators, energy storage devices, and advanced metering and control devices. The project will produce a general, extensible, and secure cyber architecture based on holonic multiagent principles to support adaptive PDS. It will produce new analytical insights to quantify the impact of information delay, quality and flow on the design and analysis of the PDS architecture. Finally, it will develop a novel approach to automating PDS with high penetration of distributed renewable resources for higher efficiency, reliability, security, and resiliency. The complex nature of future PDS will require them to adapt reactively and proactively to normal and anomalous modes of operation. The architecture produced by this project will be capable of optimizing performance and maintaining the system within operating limits during normal and minor events, such as cloud cover that reduces solar panels output. The architecture will also allow the operation of a distribution system as an island in emergencies, such as hurricanes/earthquakes, grid failures, or terrorist acts. The project will inspire future engineers via a simulation that will allow students to inject faults, failures, and weather events to see how an intelligent PDS will respond. These activities will combine cyber- and physical expertise, thus creating a workforce prepared for tomorrow?s cyber-physical system challenges. Existing university programs will be used to involve under-represented minorities and U.S. veterans in the project.

The national transmission networks that deliver high voltage electric power underpin our society and are central to the ongoing transformation of the American energy infrastructure. Transmission networks are very large and complicated engineering systems, and "keeping the lights on" as the transformation of the American energy infrastructure proceeds is a fundamental engineering challenge involving both the physical aspects of the equipment and the cyber aspects of the controls, communications, and computers that run the system. The project develops new principles of cyber-physical engineering by focusing on instabilities of electric power networks that can cause blackouts. It proposes novel approaches to analyze these instabilities and to design cyber-physical control methods to monitor, detect, and mitigate them. The controls must perform robustly in the presence of variability and uncertainty in electric generation, loads, communications, and equipment status, and during abnormal states caused by natural faults or malicious attacks. The research produces cyber-physical engineering methodologies that specifically help to mitigate power system blackouts and more generally show the way forward in designing robust cyber-physical systems in environments characterized by rich dynamics and uncertainty. Education and outreach efforts involve students at high school, undergraduate, and graduate levels, as well as dissemination of results to the public and the engineering and applied science communities in industry, government and universities.

This project takes the paradigm of cloud computing developed in the cyber-world and puts it into the physical world, to create a cyber-physical computing cloud, SAM-C. Unlike conventional cloud computing, SAM-C servers move in space, meaning, they are vehicles with physical constraints. The server vehicles also have sensors and actuators to create a way to re-organize mobile sensor networks in the paradigm of cloud computing. The project envisions an industry offering sensing as a service provided by the cloud. To enable this new service, the project extends the virtual machine instance fundamental to cloud computing with one new property -- virtual speed. The research terms this augmented entity a virtual vehicle and develops the theories, algorithms and protocols to realize many virtual vehicles over a network of real vehicle servers at scale. This research impacts the cloud computing industry by providing tools and theories it can use to leverage the many possible mobile server hosts in our society, e.g., cars, planes, people, and emerging vehicles like Unmanned Air Vehicles or drifters. It impacts mobile sensor networks by shifting them from an artifact built for an application to a service provided by a cloud. The inter-disciplinary research team spanning computer science, civil, and mechanical engineering impacts graduate and undergraduate teaching in systems, computer science, and control theory. The project guides K-12 students to build simple electric airplanes with sensors for greenhouse gas measurement thereby introducing young users of computation to cyber-physical cloud computing.

Cyber-physical systems regulating critical infrastructures, such as electrical grids and water networks, are increasingly geographically distributed, necessitating communication between remote sensors, actuators and controllers. The combination of networked computational and physical subsystems leads to new security vulnerabilities that adversaries can exploit with devastating consequences. A synchronized attack on the interdependent network components and physical plants can create complex and new security vulnerabilities that cannot be addressed by securing the constituent systems individually. This project takes a holistic view by utilizing the properties of physical systems to design new secure protocols and architectures for cyber-physical systems (CPS) through a unified conceptual framework, which uses models for the physical system and the communication/computation network to define precise attack models and vulnerabilities. These mathematical models are used to design algorithms and protocols with provable operational security guarantees, thus enabling the design of more trustworthy architectures and components. The algorithms, protocols, and architectures are validated on CPS testbeds targeting building, automobile, and smart-grid applications. Additionally, the research is being integrated into the curriculum via the creation of novel coursework combining the underlying control, information theory, cryptography, and embedded system concepts. By improving the protection of critical cyber-physical infrastructure against emerging threats, this research is expected to provide direct socio-economic benefits, ranging from individual organizations to a national scale. The inter-disciplinary team of this project will integrate teaching and curriculum development with the research, contributing to the training of a new generation of engineers well versed in the design of trustworthy cyber-physical systems.

Robotic devices are excellent candidates for delivering repetitive and intensive practice that can restore functional use of the upper limbs, even years after a stroke. Rehabilitation of the wrist and hand in particular are critical for recovery of function, since hands are the primary interface with the world. However, robotic devices that focus on hand rehabilitation are limited due to excessive cost, complexity, or limited functionality. A design and control strategy for such devices that bridges this gap is critical. The goals of the research effort are to analyze the properties and role of passive dynamics, defined by joint stiffness and damping, in the human hand and wrist during grasping and manipulation, and then mimic such properties in a wrist-hand exoskeleton for stroke rehabilitation. The project will culminate with device testing in collaboration with rehabilitation clinicians. A significant problem in robotic rehabilitation is how to provide assisted movement to the multiple degrees of freedom of the hand in order to restore motor coordination and function, with a system that is practical for deployment in a clinical environment. Armed with a clearer understanding of the mechanisms underlying passive dynamics and control of systems exhibiting such behavior, this project will inform the design of more effective wrist/hand rehabilitation devices that are feasible for clinical use. In addition, the proposed project will create a unique interdisciplinary environment enabling education, training, and co-advising of graduate students, undergraduate research, and significant and targeted outreach activities to underrepresented groups in science and engineering.

The national transmission networks that deliver high voltage electric power underpin our society and are central to the ongoing transformation of the American energy infrastructure. Transmission networks are very large and complicated engineering systems, and "keeping the lights on" as the transformation of the American energy infrastructure proceeds is a fundamental engineering challenge involving both the physical aspects of the equipment and the cyber aspects of the controls, communications, and computers that run the system. The project develops new principles of cyber-physical engineering by focusing on instabilities of electric power networks that can cause blackouts. It proposes novel approaches to analyze these instabilities and to design cyber-physical control methods to monitor, detect, and mitigate them. The controls must perform robustly in the presence of variability and uncertainty in electric generation, loads, communications, and equipment status, and during abnormal states caused by natural faults or malicious attacks. The research produces cyber-physical engineering methodologies that specifically help to mitigate power system blackouts and more generally show the way forward in designing robust cyber-physical systems in environments characterized by rich dynamics and uncertainty. Education and outreach efforts involve students at high school, undergraduate, and graduate levels, as well as dissemination of results to the public and the engineering and applied science communities in industry, government and universities.

This project aims to develop a computational framework and a physical platform for enabling dense networks of micro-robotic swarms for medical applications. The approach relies on a new stochastic framework for design and analysis of dense networks, as well as new fabrication and characterization methods for building and understanding bacteria propelled micro-robotic swarms. This project enhances the CPS science beyond passive networks of millimeter-scale bio-implantable devices with active networks of micro-robotic swarms that could be more effective in combating various critical diseases with minimal impact on the human body. Three major research objectives are proposed in this project: 1) Statistical physics inspired approach to the modeling and analysis of dense networks of swarms: The theory envisioned for characterizing the dynamics of dense networks of swarms aims at achieving ?beyond Turing? computation via dense networks, designing autonomous reliable communication protocols for dense networks, and estimating and controlling their performance; 2) Fabrication and steering of swarms of bacteria propelled swimming micro-robots: Large numbers of both chemotactic and magnetotactic bacteria integrated micro-robotic bodies will be fabricated using self-assembly and micro/nano-fabrication methods. Chemotaxis and magnetotaxis will be respectively used as passive and active steering mechanisms for navigating the swarms of micro-robots in small spaces to perform specified tasks; 3) Characterization of the behavior and control of bacteria propelled micro-robotic swarms: To validate and fine tune the proposed computational models, the motion and behavior of single and large numbers of bacteria propelled micro-robots will be characterized using optical and other microscopy methods. Intellectual Merit: The research breakthrough proposed herein consists of building a new physical platform for micro-robotic swarms by using attached bacteria as on-board actuators and chemotaxis and magnetotaxis as passive and active steering control methods, and developing a new computational dense network framework for designing and analyzing such stochastic micro-robotic swarms. The statistical computational framework to be developed in this study will improve understanding of swarming behavior and control of large numbers of bacteria propelled micro-robots. This framework offers an integrated approach towards CPS design that is meant to operate under uncertainty conditions, yet be able to succeed in performing a specified task through self-organization and collective behavior. This bottom-top approach is meant to improve the theoretical foundations of the current computational models of CPS. Broader Impacts: The resulting computational framework and the physical platform could be adapted to a wide range of different stochastic dense network systems ranging from migration of cancer cell populations or dynamics of virus populations to immune system support and modeling. The proposed swarms of bacteria integrated micro-robots have potential future applications in health-care for the diagnosis of diseases and targeted drug delivery inside the stagnant or low velocity fluids of the human body or the medical diagnosis inside lab-on-a-chip microfluidic devices. Such health-care applications could improve the welfare of our society. To foster learning and training of next generation CPS workforce, the PIs plan to emphasize a cross-disciplinary approach to teaching topics that are usually offered in disjoint tracks. The PIs will integrate the CPS research activities in this study into their newly developed courses, and they will also teach one of these courses jointly. As a joint international educational activity, a three-day Summer School will be held alternately in US and Europe every year on various CPS topics related to our project. This will help building a strong international CPS community and training US and European students in CPS topics. The PIs will present the research results of this project to children, K-12 students, K-12 teachers, IEEE and ACM student members, and college students inside and outside of USA through public lectures. This project and the Sloan Foundation will support underrepresented and minority graduate students in the project. Moreover, underrepresented minority undergraduate students will be trained through the CMU ICES summer outreach program called The SURE Thing and the NSF REU program.

This project addresses the impact of the integration of renewable intermittent generation in a power grid. This includes the consideration of sophisticated sensing, communication, and actuation capabilities on the system's reliability, price volatility, and economic and environmental efficiency. Without careful crafting of its architecture, the future smart grid may suffer from a decrease in reliability. Volatility of prices may increase, and the source of high prices may be more difficult to identify because of undetectable strategic policies. This project addresses these challenges by relying on the following components: (a) the development of tractable cross-layer models; physical, cyber, and economic, that capture the fundamental tradeoffs between reliability, price volatility, and economic and environmental efficiency, (b) the development of computational tools for quantifying the value of information on decision making at various levels, (c) the development of tools for performing distributed robust control design at the distribution level in the presence of information constraints, (d) the development of dynamic economic models that can address the real-time impact of consumer's feedback on future electricity markets, and finally (e) the development of cross-layer design principles and metrics that address critical architectural issues of the future grid. This project promotes modernization of the grid by reducing the system-level barriers for integration of new technologies, including the integration of new renewable energy resources. Understanding fundamental limits of performance is indispensable to policymakers that are currently engaged in revamping the infrastructure of our energy system. It is critical that we ensure that the transition to a smarter electricity infrastructure does not jeopardize the reliability of our electricity supply twenty years down the road. The educational efforts and outreach activities will provide multidisciplinary training for students in engineering, economics, and mathematics, and will raise awareness about the exciting research challenges required to create a sustainable energy future.

This project integrates digital microfluidics with thin-film photodetectors and control software to realize DNA target sensing using fluorescence. This cyberphysical vision is being realized through tight coupling between physical components, the microfluidic platform and miniaturized sensors, and cyber components, software for control, decision-making, and adaptation. Such a level of integration, decision, and controlled reconfigurability is a significant step forward in clinical diagnostics using digital microfluidic biochips. Topics being investigated include: (i) silicon-based digital microfluidics and integration of optical sensors; (ii) closed-loop operation and run-time optimization under software control; (iii) decision-tree architectures, adaptive reconfiguration, and error recovery. A complete testbed is being developed for nucleic acid identification on a fabricated chip with detection sites. Cyberphysical system integration will transform biochip use, in the same way as compilers and operating systems revolutionized computing, and design automation revolutionized chip design. Benefits to society include the potential to transform personalized medicine, home diagnostics, and portable diagnostics. Integration of digital microfluidics, optical sensing, and software control has the potential to create systems that can be used by any person, regardless of sample preparation skill. One example is the identification of bacterial DNA associated with bacterial blood infection (sepsis), which results in death if not diagnosed early (this is in the top 10 causes of death in the US). Students are being trained through a Senior Design course to understand the design