面向时空约束的CPS协同机制的形式化建模与分析

Cyber-Physical Systems (CPS) are distributed systems consisting of massive number of agents. Every agent is a hybrid system combining computation, communication and control. Different from conventional software system, the requirements of CPS involves explicit spatial-temporal properties. Besides, the behavior of individual agent depends on the environmental information from its neighboring time and space. The coordination of CPS makes the behaviors of agents in microscopic view satisfy the spatial-temporal constraints in system level. Building formal models for spatial-temporal constraints and the coordination of CPS, analyzing its effects on time and space, and determining whether the coordinated microscopic behaviors satisfy the macroscopic spatial-temporal requirements are the scientific problems that this project intends to solve. This project will propose a formalism to model the spatial-temporal properties of CPS with UTP methods. Based on that, the project will propose a coordination language and its semantical model which unifies the modeling of macroscopic specifications over time and space and microscopic coordination. A verification technique based on refinement calculus will be applied to determine the satisfaction of the coordinated behavior to the given spatial-temporal requirement.

信息物理融合系统（CPS）是由大量智能体组成的分布式系统，其中每个智能体都是一个具有计算、通信和控制能力的混成系统。由于每个智能体的可控资源和能力有限，系统任务的完成依赖于对各智能体行为的有效协同。与传统软件系统相比，CPS系统的需求规范具有显著的时空特征，每个智能体的行为也依赖于其相邻时空的环境信息，CPS协同机制需要使智能体微观行为的协同效果满足系统的宏观时空约束。如何对CPS的时空特征和协同机制建立形式化模型，分析协同机制在时空性质下的行为，并在此基础上验证微观协同行为满足宏观时空需求，是本项目拟解决的关键科学问题。本项目以UTP方法为基础，提出一套面向CPS的时空性质表示方法，并在此基础上提出针对时空约束的协同语言和语义模型，将宏观时空约束和微观协同行为统一到一个理论框架中；采用基于精化理论的形式化验证技术，判定系统微观协同行为是否满足给定的宏观时空需求。

与传统软件系统相比，信息物理融合系统（CPS）的需求规范具有显著的时空特征，每个智能体的行为也依赖于其相邻时空的环境信息。CPS协同机制需要使系统与环境的交互行为的满足给定的时空约束性质。本项目针对自动驾驶这一典型的CPS系统应用领域，围绕面向时空约束的CPS系统协同机制的建模与验证问题展开研究，具体研究内容和成果包括：（1）提出一种适合自动驾驶车辆环境的基于时空网格的时空约束描述语言，能够描写自动驾驶场景中同一时间点上不同位置之间的空间关系，并将不同时间的性质映射到时空网格中。（2）提出一种面向时空性质的CPS时空协同语言及其语义模型，该语义模型以代数语义为基础，采用UTP理论推导出与其一致的指称语义与操作语义模型，从而保证语义模型的正确性与兼容性，为CPS协同行为的分析验证提供了坚实基础。（3）在时空约束逻辑语言与协同行为建模语言的基础上，对自动驾驶决策系统的安全性开展形式化建模与分析验证。对自动驾驶时空环境信息建立抽象模型，采用概率模型对环境车辆决策的不确定性进行建模和预测，并在该不确定环境模型下对车辆自动驾驶决策行为的安全性进行定量分析，从而评估自动驾驶决策的安全性。.本项目的研究共发表学术论文8篇，其中CCF A类期刊论文1篇，CCF B类期刊论文2篇，SCI二区期刊论文1篇，CCF C类会议论文2篇。共培养博士研究生2名，硕士研究生2名。