信息物理系统中复杂并发行为的形式化建模与验证

The project is proposed according to the evolution of coalgebra theory and new development methodologies required by Cyber-Physical Systems. It aims to carry out research on the mathematical theory foundation and formal modeling, reasoning and verification methods for complex concurrent behavior of Cyber-Physical Systems, and to apply the theoretical results to the modeling, development and verification of Cyber-Physical Systems. In this project, we mainly concentrate on the following four work packages: (1) the coalgebraic foundations of Cyber-Physical Systems; (2) the formal modeling of complex concurrent behavior in Cyber-Physical Systems; (3) the theories and methods for proving theorems related to complex concurrent behavior in Cyber-Physical Systems; (4) the model checking approaches for Cyber-Physical Systems. The main important problems that will be investigated in this project include the existence of final coalgebras on the category of continuous spaces, the compositionality of coalgebras, the unified coalgebraic semantics for different software and hardware components and connectors in Cyber-Physical Systems, the coinductive reasoning and proof methods for Cyber-Physical Systems, searching best proof strategy via machine learning techniques, abstraction techniques in model checking of Cyber-Physical Systems, and so on. The proposed research may promote the development of coalgebra theory, provide rigorous formal theoretical supports for modeling, analysis and verification of Cyber-Physical Systems, and improve the correctness, confidence and safety of Cyber-Physical Systems. It offers great benefits from both theoretical and practical perspective.

本项目根据共代数理论发展和信息物理系统开发的需要提出，研究目标是开展针对信息物理系统复杂并发行为的数学理论基础以及形式化建模、推理与验证方法的研究，并将所得理论成果应用于信息物理系统的建模、开发和验证之中。研究内容重点集中在以下四方面：(1) 信息物理系统共代数理论基础；(2) 信息物理系统中复杂并发行为形式化建模；(3) 信息物理系统中复杂并发行为相关定理证明理论及方法；(4) 信息物理系统模型检验方法。本项目主要对连续空间范畴上终结共代数存在性及共代数可组合性、信息物理系统不同组件和连接件的统一共代数语义、信息物理系统共归纳推理与证明方法、通过机器学习方法寻找最佳证明策略、信息物理系统模型检验中的抽象技术等重要问题进行研究。所得结果对于推动共代数理论的发展，为信息物理系统的建模、分析和验证提供严格的形式化理论支持，提高信息物理系统的正确性、可信性和安全性，在理论和实践上都具有重要意义。

信息物理系统是深度融合了计算、通信和控制能力的可控、可信、可扩展的复杂系统，通过计算进程和物理进程的并发和交互实现系统的功能，由于信息物理系统行为的复杂性，特别是系统中不同组件之间并发交互行为的开放、动态、非确定性，使得对信息物理系统行为的正确性保障成为国际上面临的科学难题和重大挑战。在此背景下，本项目开展了针对信息物理系统并发行为的共代数理论基础以及形式化建模、推理与验证方法的研究，并将所得理论成果应用于信息物理系统的建模、开发和验证之中。项目研究内容重点集中在以下四方面：(1)信息物理系统共代数理论基础；(2)信息物理系统中复杂并发行为形式化建模；(3)信息物理系统中复杂并发行为相关定理证明理论及方法；(4)信息物理系统模型检验方法。取得的重要成果包括：(1)对建模语言Reo的随机实时扩展、基于该扩展语言的概率时间计算树逻辑以及相关的模型检验算法的实现；(2)信息物理系统建模语言Mediator及其概率和分布式扩展的设计，以及代码生成、模型检验等相关工具的实现；(3)基于共归纳原理的信息物理系统复杂并发行为相关性质验证的定理证明方法，以及通过定理证明与SMT约束求解技术的集成在定理证明方法无法判定性质是否可证时对可能的有界反例的自动搜索；(4)针对深度神经网络的抽象自动机模型提取和全局鲁棒性验证框架；(5)深度学习系统良性数据以及对抗样本非确定性度量标准为向导的测试方法；(6)可用于刻画信息物理系统中并发行为的概率时间特性的时间数据分布流理论模型及其在定理证明器中的共归纳定义；(7)多种量子系统的共代数语义定义及终结共代数的存在性；(8)模糊系统的共代数模型及组合算子的定义；(9)基于深度学习和数据挖掘技术的证明策略推荐方法。本项目中所取得的成果对于推动共代数理论的发展，为信息物理系统的建模、分析和验证提供严格的形式化理论支持，提高信息物理系统的正确性、可信性和安全性，在理论和实践上都具有重要意义。