面向时空约束的CPS协同机制的形式化建模与分析
结题报告
批准号:
61602177
项目类别:
青年科学基金项目
资助金额:
20.0 万元
负责人:
李钦
依托单位:
学科分类:
F0201.计算机科学的基础理论
结题年份:
2019
批准年份:
2016
项目状态:
已结题
项目参与者:
朱龙飞、叶昕、李新、刘艾伦、卢建宇
国基评审专家1V1指导 中标率高出同行96.8%
结合最新热点,提供专业选题建议
深度指导申报书撰写,确保创新可行
指导项目中标800+,快速提高中标率
客服二维码
微信扫码咨询
中文摘要
信息物理融合系统(CPS)是由大量智能体组成的分布式系统,其中每个智能体都是一个具有计算、通信和控制能力的混成系统。由于每个智能体的可控资源和能力有限,系统任务的完成依赖于对各智能体行为的有效协同。与传统软件系统相比,CPS系统的需求规范具有显著的时空特征,每个智能体的行为也依赖于其相邻时空的环境信息,CPS协同机制需要使智能体微观行为的协同效果满足系统的宏观时空约束。如何对CPS的时空特征和协同机制建立形式化模型,分析协同机制在时空性质下的行为,并在此基础上验证微观协同行为满足宏观时空需求,是本项目拟解决的关键科学问题。本项目以UTP方法为基础,提出一套面向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系统协同机制的建模与验证问题展开研究,具体研究内容和成果包括:(1)提出一种适合自动驾驶车辆环境的基于时空网格的时空约束描述语言,能够描写自动驾驶场景中同一时间点上不同位置之间的空间关系,并将不同时间的性质映射到时空网格中。(2)提出一种面向时空性质的CPS时空协同语言及其语义模型,该语义模型以代数语义为基础,采用UTP理论推导出与其一致的指称语义与操作语义模型,从而保证语义模型的正确性与兼容性,为CPS协同行为的分析验证提供了坚实基础。(3)在时空约束逻辑语言与协同行为建模语言的基础上,对自动驾驶决策系统的安全性开展形式化建模与分析验证。对自动驾驶时空环境信息建立抽象模型,采用概率模型对环境车辆决策的不确定性进行建模和预测,并在该不确定环境模型下对车辆自动驾驶决策行为的安全性进行定量分析,从而评估自动驾驶决策的安全性。.本项目的研究共发表学术论文8篇,其中CCF A类期刊论文1篇,CCF B类期刊论文2篇,SCI二区期刊论文1篇,CCF C类会议论文2篇。共培养博士研究生2名,硕士研究生2名。
期刊论文列表
专著列表
科研奖励列表
会议论文列表
专利列表
DOI:10.1109/access.2019.2943184
发表时间:2019
期刊:IEEE Access
影响因子:3.9
作者:Xu Bingqing;Li Qin;Guo Tong;Du Dehui
通讯作者:Du Dehui
A new roadmap for linking theories of programming and its applications on GCL and CSP
连接编程理论及其在 GCL 和 CSP 上的应用的新路线图
DOI:10.1016/j.scico.2017.10.009
发表时间:2017-11
期刊:Science of Computer Programming
影响因子:1.3
作者:He Jifeng;Li Qin
通讯作者:Li Qin
DOI:10.15439/2018f148
发表时间:2018-09
期刊:Communication Papers of the 2018 Federated Conference on Computer Science and Information Systems
影响因子:--
作者:Longfei Zhu;Qiwen Xu;Huibiao Zhu
通讯作者:Huibiao Zhu
DOI:10.1080/0952813x.2018.1544203
发表时间:2018-11
期刊:Journal of Experimental & Theoretical Artificial Intelligence
影响因子:2.2
作者:Gou Genwang;Zhao Yongxin;Li Qin;Xu Qiwen
通讯作者:Xu Qiwen
Isolation Modeling and Analysis Based on Mobility
基于移动性的隔离建模与分析
DOI:10.1145/3306606
发表时间:2019
期刊:ACM Transactions on Software Engineering and Methodology
影响因子:4.4
作者:Jian-Min Jiang;Huibiao Zhu;Qin Li;Yongxin Zhao;Zhong Hong;Shi Zhang;Ping Gong
通讯作者:Ping Gong
面向智能网联车的时空认知多粒度分解与协同机制的建模与验证
  • 批准号:
    --
  • 项目类别:
    面上项目
  • 资助金额:
    54万元
  • 批准年份:
    2022
  • 负责人:
    李钦
  • 依托单位:
国内基金
海外基金