Equipment operation represents one of the most dangerous tasks on a construction sites and accidents related to such operation often result in death and property damage on the construction site and the surrounding area. Such accidents can also cause considerable delays and disruption, and negatively impact the efficiency of operations. This award will conduct research to improve the safety and efficiency of cranes by integrating advances in robotics, computer vision, and construction management. It will create tools for quick and easy planning of crane operations and incorporate them into a safe and efficient system that can monitor a crane's environment and provide control feedback to the crane and the operator. Resulting gains in safety and efficiency will reduce fatal and non-fatal crane accidents. Partnerships with industry will also ensure that these advances have a positive impact on construction practice, and can be extended broadly to smart infrastructure, intelligent manufacturing, surveillance, traffic monitoring, and other application areas. The research will involve undergraduates and includes outreach to K-12 students. The work is driven by the hypothesis that the monitoring and control of cranes can be performed autonomously using robotics and computer vision algorithms, and that detailed and continuous monitoring and control feedback can lead to improved planning and simulation of equipment operations. It will particularly focus on developing methods for (a) planning construction operations while accounting for safety hazards through simulation; (b) estimating and providing analytics on the state of the equipment; (c) monitoring equipment surrounding the crane operating environment, including detection of safety hazards, and proximity analysis to dynamic resources including materials, equipment, and workers; (d) controlling crane stability in real-time; and (e) providing feedback to the user and equipment operators in a "transparent cockpit" using visual and haptic cues. It will address the underlying research challenges by improving the efficiency and reliability of planning through failure effects analysis and creating methods for contact state estimation and equilibrium analysis; improving monitoring through model-driven and real-time 3D reconstruction techniques, context-driven object recognition, and forecasting motion trajectories of objects; enhancing reliability of control through dynamic crane models, measures of instability, and algorithms for finding optimal controls; and, finally, improving efficiency of feedback loops through methods for providing visual and haptic cues.

Cyber-physical systems (CPS) encompass the next generation of computerized control for countless aspects of the physical world and interactions thereof. The typical engineering process for CPS reuses existing designs, models, components, and software from one version to the next. For example, in automotive engineering, it is common to reuse significant portions of existing model-year vehicle designs when developing the next model-year vehicle, and such practices are common across CPS industries, from aerospace to biomedical. While reuse drastically enhances efficiency and productivity, it leads to the possibility of introducing unintended mismatches between subcomponents' specifications. For example, a 2011 US National Highway Traffic Safety Administration (NHTSA) recall of over 1.5 million model-year 2005-2010 vehicles was due to the upgrade of a physical transmission component that was not appropriately addressed in software. A mismatch between cyber and physical specifications may occur when a software or hardware upgrade (in effect, a cyber or physical specification change) is not addressed by an update (in effect, a matching specification change) in the other domain. This research will develop new techniques and software tools to detect automatically if cyber-physical specification mismatches exist, and then mitigate the effects of such mismatches at runtime, with the overall goal to yield more reliable and safer CPS upon which society increasingly depends. The detection and mitigation methods developed will be evaluated in an energy CPS testbed. While the evaluation testbed is in the energy domain, the methods are applicable to other CPS domains such as automotive, aerospace, and biomedical. The educational goals will bridge gaps between computer science and electrical engineering, preparing a diverse set of next-generation CPS engineers by developing education platforms to enhance CPS engineering design and verification skills. The proposed research is to develop new techniques and tools to automatically identify and mitigate the effects of cyber-physical specification mismatches. There are three major research objectives. The first objective is to identify cyber-physical specification mismatches. To identify mismatches, a detection problem will be formalized using the framework of hybrid input/output automata (HIOA). Offline algorithms will be designed to find candidate specifications from models and implementations using static and dynamic analyses, and then identify candidate mismatches. The second objective is to monitor and assure safe CPS upgrades. As modern CPS designs are complex, it may be infeasible to determine all specifications and mismatches between all subcomponents at design time. Runtime monitoring and verification methods will be developed for inferred specifications to detect mismatches at runtime. When they are identified, a runtime assurance framework building on supervisory control and the Simplex architecture will assure safe CPS runtime operation. The third objective is to evaluate safe CPS upgrades in an example CPS. The results of the other objectives and their ability to ensure safe CPS upgrades will be evaluated in an energy CPS testbed, namely an AC electrical distribution microgrid that interfaces DC-producing renewables like photovoltaics to AC.

Title: CPS: Breakthrough: Development of Novel Architectures for Control and Diagnosis of Safety-Critical Complex Cyber-Physical Systems This project is developing novel architectures for control and diagnosis of complex cyber-physical systems subject to stringent performance requirements in terms of safety, resilience, and adaptivity. These ever-increasing demands necessitate the use of formal model-based approaches to synthesize provably-correct feedback controllers. The intellectual merit of this research lies in a novel combination of techniques from the fields of dynamical systems, discrete event systems, reactive synthesis, and graph theory, together with new advancements in terms of abstraction techniques, computationally efficient synthesis of control and diagnosis strategies that support distributed implementations, and synthesis of acquisition of information and communication strategies. The project's broader significance and importance are demonstrated by the expected improvement of the safety, resilience, and performance of complex cyber-physical systems in critical infrastructures as well as the efficiency with which they are designed and certified. The original approach being developed is based on the combination of multi-resolution abstraction graphs for building discrete models of the underlying cyber-physical system with reactive synthesis techniques that exploit a representation of the solution space in terms of a finite structure called a decentralized bipartite transition system. The concepts of abstraction graph and decentralized bipartite transition system are novel and open new avenues of investigation with significant potential to the formal synthesis of safe, resilient, and adaptive controllers. This methodology naturally results in a set of decentralized and asynchronous controllers and diagnosers, which ensures greater resilience and adaptivity. Overall, this research will significantly impact the Science of Cyber-Physical Systems and the Engineering of Cyber-Physical Systems.

This project establishes a new framework for the formal verification of cyber-physical systems. The framework combines the power of logical decision engines and scalable numerical methods to perform safety verification of general nonlinear hybrid systems. The key difficulty with formal verification of hybrid systems is that all scalable modern verification techniques rely heavily on the use of powerful decision procedures. For hybrid systems, one needs to reason about logic formulas over the real numbers with nonlinear functions, which has been regarded as an intractable problem. The project proposes new directions for tackling the core decision problems, with the combined power of logical and numerical algorithms. The research directly leads to the development of practical tools that will push the frontier of verification of realistic cyber-physical systems to a brand new level. This project aims at fundamental research of problems that stand at the core of the design, analysis, and implementation of reliable cyber-physical systems. It combines techniques from logic, numerical analysis, and automated reasoning, and will produce a unifying methodology that is powerful to address main challenges in this field. The techniques developed in this project will significantly enhance the complexity and reliability of the next generations of cyber-physical systems. Cyber-physical systems are ubiquitous in safety-critical applications as diverse as aerospace, automotive, civil infrastructure, energy, manufacturing, and healthcare. Malfunctioning cyber-physical systems can have catastrophic economic and societal consequences. This project will have a broad range of impact in these areas. This research aims to significantly enhance the management of complexity and reliability of the next generations of cyber-physical systems, and will broadly impact all the application areas.

Until now, the "cyber" component of automobiles has consisted of control algorithms and associated software for vehicular subsystems designed to achieve one or more performance, efficiency, reliability, comfort, or safety goals, primarily based on short-term intrinsic vehicle sensor data. However, there exist many extrinsic factors that can affect the degree to which these goals can be achieved. These factors can be determined from: longer-term traces of in-built sensor data that can be abstracted as triplines, socialized versions of these that are shared amongst vehicle users, and online databases. These three sources of information collectively constitute the automotive infoverse. This project harnesses this automotive infoverse to achieve these goals through high-confidence vehicle tuning and driver feedback decisions. Specifically, the project develops software called Headlight that permits the rapid development of apps that use the infoverse to achieve one or more goals. Advisory apps can provide feedback to the driver in order to ensure better fuel efficiency, while auto-tuning goals can set car parameters to promote safety. Allowing vehicles and such apps to share vehicle data with others and to use extrinsic information results in novel information processing, assurance, and privacy challenges. The project develops methods, algorithms and models to address these challenges. Broader Impact - This project can have significant societal impact by reducing carbon emissions and improving vehicular safety, can spur innovation in tuning methods and encourage researchers to experiment with this class of cyber-physical systems. The active participation of General Motors will strongly facilitate technology transfer. There is significant outreach including high school student participation, undergraduate research activities, internships, and creation of an open framework for plug and play application developers to use.

Multicore platforms have the potential of revolutionizing the capabilities of embedded cyber-physical systems. Unfortunately, when such systems have safety-critical components, multicore platforms are rarely used. The reason is a lack of predictability associated with hardware components such as caches, memory controllers, etc., that are shared among cores. With current technology, very conservative estimates concerning the usage of these shared resources must be made, to certify that overuse violations do not occur at runtime. The resulting over-provisioning can be significant, easily negating the processing power of any additional cores. The goal of this project is to resolve this multicore "predictability problem" by developing allocation mechanisms that enable shared hardware resources to be controlled in a predictable way. The research agenda in this project includes fundamental research on relevant real-time resource allocation problems, prototyping efforts involving real-time operating systems and middleware, and experimental evaluations of improvements enabled by the developed mechanisms in timing analysis tools (which are used to determine task execution-time budgets). Addressing the "predictability problem" associated with multicore platforms would be a breakthrough result for safety-critical, cyber-physical systems in domains such as avionics and automobiles. When using multicore platforms to host highly-critical workloads in these domains, the current state of the art is to obviate the predictability problem by turning off all but one core. Unless a more intelligent solution can be found, such domains will not benefit from savings in size, weight, and power (SWaP) and gains in functionality that multicore platforms afford. Broader impacts include joint research with industry colleagues on supporting real-time workloads in unmanned air vehicles, the development of publicly-available open-source software that can be used by other institutions for research and teaching purposes, and the development of a new course on cyber-physical systems.

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.