CPS: Breakthrough: A Mathematical Theory of Cyber-Physical Systems

CPS：突破：网络物理系统的数学理论

• 批准号: 1446619
• 负责人: Edward Lee
• 金额: $ 49.93万
• 依托单位: University of California-Berkeley
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2015
• 资助国家: 美国
• 起止时间: 2015-01-01 至 2018-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1446619&HistoricalAwards=false
• 关键词: CPS; Breakthrough; Mathematical; Theory; Cyber

Title: CPS: Breakthrough: A Mathematical Theory of Cyber-Physical SystemsThe 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.

职务名称：CPS：突破：网络物理系统的数学理论网络物理系统的根本挑战是网络和物理系统的不同科学和工程模型，方法和工具的融合。网络系统主要是处理信息。物理系统主要是关于结构和动力学，即状态随时间的演化。该项目开发了一个网络物理系统的数学理论，提供了网络和物理之间的正式接口。该项目的智力优势是建模和设计以及网络物理系统的实施和验证的坚实基础，以及网络物理系统工程与标准数学实践的新兴学科的富有成效的联系。该项目的广泛意义和重要性为评估网络物理系统技术提供了坚实的基础，并使信息物理系统工程学科发展成为一个成熟和持久的研究领域。该项目基于广义超度量半格理论和广义超度量半格上严格收缩函数的不动点理论，开发了一个信息物理系统工程学科，物理域理论，为任意组成和高阶行为提供坚实的数学基础，为网络物理计算制定正确的收敛和连续性概念，并发展近似和有效性概念，允许理论抽象和实践实现之间的双向联系。它进一步将该理论应用于广泛的建模和模拟混合离散和连续现象的经典问题，并将其扩展到包括网络子系统对其在网络物理系统中的物理对应物的离散干预。它还研究了该理论对网络物理系统的实现和验证的实际影响，通过该理论的棱镜重新检查当前使用的计算时间模型，探索具有在理论抽象上完成的时间结构的编程语言的扩展，并将理论集成到自动和交互式定理证明器中，以补充现有的模型检查方法，这些方法可能会屈服于网络物理系统的规模。