The objective of this research is to address fundamental challenges in the verification and analysis of reconfigurable distributed hybrid control systems. These occur frequently whenever control decisions for a continuous plant depend on the actions and state of other participants. They are not supported by verification technology today. The approach advocated here is to develop strictly compositional proof-based verification techniques to close this analytic gap in cyber-physical system design and to overcome scalability issues. This project develops techniques using symbolic invariants for differential equations to address the analytic gap between nonlinear applications and present verification techniques for linear dynamics. This project aims at transformative research changing the scope of systems that can be analyzed. The proposed research develops a compositional proof-based approach to hybrid systems verification in contrast to the dominant automata-based verification approaches. It represents a major improvement addressing the challenges of composition, reconfiguration, and nonlinearity in system models The proposed research has significant applications in the verification of safety-critical properties in next generation cyber-physical systems. This includes distributed car control, robotic swarms, and unmanned aerial vehicle cooperation schemes to full collision avoidance protocols for multiple aircraft. Analysis tools for distributed hybrid systems have a broad range of applications of varying degrees of safety-criticality, validation cost, and operative risk. Analytic techniques that find bugs or ensure correct functioning can save lives and money, and therefore are likely to have substantial economic and societal impact.

The objective of this research is to study the formal design and verification of advanced vehicle dynamics control systems. The approach is to consider the vehicle-driver-road system as a cyber-physical system (CPS) by focusing on three critical components: (i) the tire-road interaction; (ii) the driver-vehicle interaction; and (iii) the controller design and validation. Methods for quantifying and estimating the uncertainty of the road friction coefficient by using self-powered wireless sensors embedded in the tire are developed for considering tire-road interaction. Tools for real-time identification of nominal driver behavior and uncertainty bounds by using in-vehicle cameras and body wireless sensors are developed for considering driver-vehicle interaction. A predictive hybrid supervisory control scheme will guarantee that the vehicle performs safely for all possible uncertainty levels. In particular, for controller design and validation, the CPS autonomy level is continuously adapted as a function of human and environment conditions and their uncertainty bounds quantified by considering tire-road and driver-vehicle interaction. High confidence is critical in all human operated and supervised cyber-physical systems. These include environmental monitoring, telesurgery, power networks, and any transportation CPS. When human and environment uncertainty bounds can be predicted, safety can be robustly guaranteed by a proper controller design and validation. This avoids lengthy and expensive trial and error design procedures and drastically increases their confidence level. Graduate, undergraduate and underrepresented engineering students benefit from this project through classroom instruction, involvement in the research and substantial interaction with industrial partners from the fields of tires, vehicle active safety, and wireless sensors.

The objective of this research is to develop a framework for the development and deployment of next-generation medical systems consisting of integrated and cooperating medical devices. The approach is to design and implement an open-source medical device coordination framework and a model-based component oriented programming methodology for the device coordination, supported by a formal framework for reasoning about device behaviors and clinical workflows. The intellectual merit of the project lies in the formal foundations of the framework that will enable rapid development, verification, and certification of medical systems and their device components, as well as the clinical scenarios they implement. The model-based approach will supply evidence for the regulatory approval process, while run-time monitoring components embedded into the system will enable "black box" recording capabilities for the forensic analysis of system failures. The open-source distribution of tools supporting the framework will enhance its adoption and technology transfer. A rigorous framework for integrating and coordinating multiple medical devices will enhance the implementation of complicated clinical scenarios and reduce medical errors in the cases that involve such scenarios. Furthermore, it will speed up and simplify the process of regulatory approval for coordination-enabled medical devices, while the formal reasoning framework will improve the confidence in the design process and in the approval decisions. Overall, the framework will help reduce costs and improve the quality of the health care.

The objective of this research is to investigate and develop methods and tools for the analysis and verification of cyber-physical systems. The approach is to augment the methods and tools that have been developed at the University of Utah and the University of South Florida for modeling and verification of asynchronous and analog/mixed-signal circuits to address challenges in cyber-physical system verification. This research will develop a unified framework with methods and tools which include an integrated formalism to comprehensively model discrete/continuous, functional/timing, synchronous/asynchronous, and deterministic/stochastic behavior. These tools will also include algorithms to analyze behavior and verify that it satisfies the correctness requirements on functionality, timing, and robustness. Finally, they will include abstraction and compositional reasoning approaches to enable large systems to be analyzed and verified efficiently. Since cyber-physical systems are becoming ubiquitous, improvements in such systems such as higher reliability, better fault-tolerance, improved performance, and lower design costs will have tremendous positive impact on society. Results from this research will be transferred to the cyber-physical systems community and other application domains by both publishing papers in related conferences and journals as well as by freely distributing tools via the Internet. Both graduate and undergraduate students will be engaged in this multi-institutional research where they will be exposed to the latest research in formal and probabilistic analysis. Early involvement of undergraduate students may help encourage them to attend graduate school. This research project will also recruit underrepresented and female students to allow it to reach broader audiences.

The objective of this research is to investigate and develop methods and tools for the analysis and verification of cyber-physical systems. The approach is to augment the methods and tools that have been developed at the University of Utah and the University of South Florida for modeling and verification of asynchronous and analog/mixed-signal circuits to address challenges in cyber-physical system verification. This research will develop a unified framework with methods and tools which include an integrated formalism to comprehensively model discrete/continuous, functional/timing, synchronous/asynchronous, and deterministic/stochastic behavior. These tools will also include algorithms to analyze behavior and verify that it satisfies the correctness requirements on functionality, timing, and robustness. Finally, they will include abstraction and compositional reasoning approaches to enable large systems to be analyzed and verified efficiently. Since cyber-physical systems are becoming ubiquitous, improvements in such systems such as higher reliability, better fault-tolerance, improved performance, and lower design costs will have tremendous positive impact on society. Results from this research will be transferred to the cyber-physical systems community and other application domains by both publishing papers in related conferences and journals as well as by freely distributing tools via the Internet. Both graduate and undergraduate students will be engaged in this multi-institutional research where they will be exposed to the latest research in formal and probabilistic analysis. Early involvement of undergraduate students may help encourage them to attend graduate school. This research project will also recruit underrepresented and female students to allow it to reach broader audiences.