面向信息物理融合系统的程序统一理论研究

Cyber-Physical System (CPS for short) is a new generation system, which is deeply connected by computing, communication and control, enhancing the ability of physical systems through networked computing. Unifying Theories of Programming (UTP for short) was developed by C.A.R. Hoare (Turing Award Winner) and Jifeng He in 1998, which has been recognized as an outstanding method for various programming. This project is devoted to investigate UTP for CPS, focusing on the mixing of continuous/discrete, time-space consistency, collaboration and networking. The study of this project includes constructing modeling languages for the features of CPS, investigating the denotational semantics, algebra semantics, operational semantics and deduction system, aiming to support the correct description and property verification for CPS. This project also explores the consistency among the four formal models from different viewpoints, ensuring the correctness of the semantical models and deduction system. Based on the theoretical achievements of formal semantics and deduction system, the analysis and verification of typical case studies is also studied. The investigation of this project will make meaningful extensions for UTP and provide theoretical support for the safety of CPS.

信息物理融合系统是计算、通讯和控制深度交联，通过网络化计算增强物理系统能力的新一代系统。程序统一理论是由图灵奖获得者C.A.R. Hoare教授和华东师范大学何积丰院士于1998年提出，已经被国际上公认为研究各类程序的一种优秀的方法。本项目针对信息物理融合系统的连续离散融合、时空一致性、协同性、网络化等特性，致力于面向信息物理融合系统的程序统一理论的研究。为信息物理融合系统的典型特性构建建模语言，研究其指称语义、代数语义、操作语义及证明系统，支持信息物理融合系统精确的行为刻画和性质验证。采用不同的视角研究这四种形式化模型的一致性，为语义模型和证明系统的正确性提供了形式化保证。基于形式语义和证明系统的理论成果，开展信息物理融合系统典型案例的分析验证。本项目的研究将对程序统一理论产生理论意义的拓展，并对信息物理融合系统的安全性提供理论支持。

信息物理融合系统(CPS)是计算、通讯和控制深度交联，通过网络化计算增强物理系统能力的新一代系统。程序统一理论(UTP)是由图灵奖获得者C.A.R. Hoare教授和华东师范大学何积丰院士于1998年提出，已经被国际上公认为研究各类程序的一种优秀的方法。本项目面向若干特定CPS领域，针对建模语言的构造及相应的UTP理论，开展了一系列的研究。. 首先，对于MDESL建模语言，我们从理论和实践两个角度开展了UTP理论的相关研究，主要包括MDESL代数语义和操作语义连接的理论和机械证明，以及MDESL指称语义和代数语义的理论和机械研究。从理论和实践的角度对操作语义的正确性和完备性及代数定律的正确性进行了验证。其中，机械证明和研究都是基于定理证明器Coq完成的。同时，我们构造了移动分布式系统的进程演算BigrTiMo，演算不但捕捉了移动计算的移动性，还刻画了移动计算的空间结构和时间特性，我们开展了其操作语义、指称语义、代数语义、证明系统以及语义连接的研究。此外，传统的CPS系统大多基于通讯进行信息交互，我们构造了基于共享变量的CPS系统建模语言，并研究了其指称语义、代数语义和证明系统。其中，指称语义和证明系统都是基于轨迹模型。针对物联网和移动边缘计算等网络化系统，我们也开展了其UTP语义的研究。最后，我们以车联网为案例开展了CPS系统的验证研究。