Visible to the public CPS: Breakthrough: A Mathematical Theory of Cyber-Physical SystemsConflict Detection Enabled

Project Details
Lead PI:Edward Lee
Performance Period:01/01/15 - 12/31/17
Institution(s):University of California at Berkeley
Sponsor(s):National Science Foundation
Award Number:1446619
537 Reads. Placed 300 out of 803 NSF CPS Projects based on total reads on all related artifacts.
Abstract: Title: CPS: Breakthrough: A Mathematical Theory of Cyber-Physical Systems The fundamental challenge in cyber-physical systems is the confluence of distinct scientific and engineering models, methods, and tools for cyber and physical systems. Cyber systems are primarily about processing information. Physical systems are primarily about structure and dynamics, the evolution of state in time. This project develops a mathematical theory of cyber-physical systems that provides a formal interface between the cyber and the physical. The intellectual merits of the project are a solid basis for the modeling and design as well as the implementation and verification of cyber-physical systems, and a fruitful connection of the nascent discipline of cyber-physical-systems engineering with standard mathematical practice. The project's broader significance and importance are providing a sound foundation by which cyber-physical system technologies can be assessed, and enabling the discipline of cyber-physical-system engineering to evolve into a mature and durable field of study. The project builds on the theory of generalized ultrametric semilattices and the fixed-point theory of strictly contracting functions on generalized ultrametric semilattices to develop a cyber-physical domain theory, providing a firm mathematical footing for arbitrary composition and higher-order behavior, formulating the right notion of convergence and continuity for cyber-physical computation, and developing a notion of approximation and effectiveness that allows for a two-way connection between the abstractions of the theory and the realizations of practice. It further applies the theory to a wide range of classic problems of modeling and simulating mixed discrete and continuous phenomena, and extends it to embrace the discrete interventions of a cyber subsystem on its physical counterpart in a cyber-physical system. It also investigates the practical implications of the theory for the implementation and verification of cyber-physical systems by reexamining currently used timed models of computation through the prism of the theory, exploring the extension of programming languages with temporal constructs that are complete over the theoretical abstractions, and integrating the theory in automated and interactive theorem provers to supplement existing model-checking methods that might succumb to the scale of cyber-physical systems.