多机器人路径规划的安全性验证

发布时间：2018-02-25 10:12

  本文关键词： 人工智能 机器人 混成通信顺序进程 混成系统 形式化验证 定理证明　出处：《软件学报》2017年05期 　论文类型：期刊论文

【摘要】：近年来,伴随着人工智能领域的浪潮,机器人越来越多地出现在我们的日常生活中,例如足球机器人、无人机、无人车等.如何保证这些自治机器人尤其是多个机器人在移动过程中的安全,成为人们一直很关心的问题.混成通信顺序进程(hybrid communicating sequential process,简称HCSP)是一种针对混成系统的形式化建模语言,在通信顺序进程(communicating sequential process,简称CSP)的基础上引入了微分方程以描述混成系统中的连续行为和控制逻辑,可以方便而高效地对大型控制系统,尤其是在有通信事件发生时的情形进行形式化建模.用HCSP建模多机器人的路径控制算法,并用定理证明工具HProver进行形式化验证,结果表明,在满足一定的初始条件下,机器人团队在整个运行途中不会发生碰撞.
[Abstract]:In recent years, with the tide of artificial intelligence, robots are more and more popular in our daily life, such as soccer robots, drones, How to ensure the safety of these autonomous robots, especially multiple robots, in the process of moving, Hybrid communicating sequential process is a formal modeling language for hybrid communicating sequential process. On the basis of communication sequence sequential process, differential equation is introduced to describe the continuous behavior and control logic in the hybrid system. HCSP is used to model the path control algorithm of multi-robot, and the theorem proving tool HProver is used to formally verify the algorithm. The results show that, under certain initial conditions, the model can be used to model the path control algorithm of multi-robot, especially in the case of communication event. The robot team does not collide during the entire run.
【作者单位】： 计算机科学国家重点实验室(中国科学院软件研究所);
【基金】：国家自然科学基金(91118007,6110006,61304185)~~
【分类号】：TP311

【参考文献】

相关期刊论文 前1条

1 郭丹青;吕继东;王淑灵;唐涛;詹乃军;周达天;邹亮;;中国高速铁路列控系统的形式化分析与验证[J];中国科学:信息科学;2015年03期

【共引文献】

相关期刊论文 前2条

1 刘涛;王淑灵;詹乃军;;多机器人路径规划的安全性验证[J];软件学报;2017年05期

2 AHMAD Ehsan;DONG YunWei;LARSON Brian;Lü JiDong;TANG Tao;ZHAN NaiJun;;Behavior modeling and verification of movement authority scenario of Chinese Train Control System using AADL[J];Science China(Information Sciences);2015年11期

【二级参考文献】

相关期刊论文 前2条

1 徐田华;赵红礼;唐涛;;基于有色Petri网的ETCS无线通信可靠性分析[J];铁道学报;2008年01期

2 唐涛,郜春海;ETCS系统分析及CTCS的研究[J];机车电传动;2004年06期

【相似文献】

相关期刊论文 前10条

1 李浪;李仁发;李肯立;姚凤娟;;混成系统研究综述[J];计算机应用研究;2008年08期

2 侯建民,郑滔,樊晓聪,李宣东,郑国梁;线性混成系统的参数分析[J];计算机学报;1999年06期

3 范双南;;基于时间序列分析的混成系统可靠性评价方法[J];福建电脑;2011年03期

4 邹进;林望;罗勇;曾振柄;;基于多面体包含的非线性混成系统可达性分析[J];计算机应用;2013年05期

5 卜磊;解定宝;;混成系统形式化验证[J];软件学报;2014年02期

6 乔磊;齐骥;龚育昌;;一种支持可重构混成系统的操作系统设计与实现[J];计算机学报;2009年05期

7 赵剑;欧阳丹彤;王晓宇;张立明;;混成系统的分布式诊断方法[J];吉林大学学报(工学版);2012年06期

8 肖娟;;混成系统的形式验证[J];长沙通信职业技术学院学报;2008年01期

9 叶林;汤瀑;郭立鹏;张亮;;基于混成系统的物联网服务建模与验证[J];小型微型计算机系统;2013年12期

10 阎安,唐稚松;基于 XYZ/ E的混成系统(英文)[J];软件学报;2000年01期

相关会议论文 前1条

1 任雁;田婕;孙辉;周永;;混成系统测试研究综述[A];2011年通信与信息技术新进展——第八届中国通信学会学术年会论文集[C];2011年

相关博士学位论文 前6条

1 解定宝;混成系统有界模型检验优化技术研究[D];南京大学;2016年

2 王国滨;信息物理融合系统安全性验证研究[D];华东师范大学;2016年

3 林望;基于符号数值混合计算的混成系统可信分析与验证研究[D];华东师范大学;2013年

4 赵剑;混成系统基于模型诊断的若干问题研究[D];吉林大学;2012年

5 孔辉;基于归纳不变式的混成系统安全性验证[D];清华大学;2013年

6 李广元;LTLC：面向实时与混成系统的连续时序逻辑[D];中国科学院软件研究所;2001年

相关硕士学位论文 前7条

1 杨阳;基于深度优先搜索的混成系统有界可达性分析[D];南京大学;2013年

2 蒋慧;基于迁移系统语义的线性混成系统分析[D];南京大学;2013年

3 李国拯;基于组合形式规范的混成系统形式化验证方法研究[D];南京航空航天大学;2015年

4 邹进;非线性混成系统的可达性分析[D];温州大学;2013年

5 李倩;基于形式化方法的混成系统安全性检验[D];华东师范大学;2015年

6 钱宇清;Hybrid AADL：混成系统体系结构分析与设计语言[D];华东师范大学;2014年

7 钱磊;信息物理融合系统的形式化建模与讨论[D];华东师范大学;2013年

，

本文编号：1534003