發(fā)布時間：2018-02-25 10:12

  本文關(guān)鍵詞： 人工智能 機器人 混成通信順序進(jìn)程 混成系統(tǒng) 形式化驗證 定理證明　出處：《軟件學(xué)報》2017年05期 　論文類型：期刊論文

【摘要】：近年來,伴隨著人工智能領(lǐng)域的浪潮,機器人越來越多地出現(xiàn)在我們的日常生活中,例如足球機器人、無人機、無人車等.如何保證這些自治機器人尤其是多個機器人在移動過程中的安全,成為人們一直很關(guān)心的問題.混成通信順序進(jìn)程(hybrid communicating sequential process,簡稱HCSP)是一種針對混成系統(tǒng)的形式化建模語言,在通信順序進(jìn)程(communicating sequential process,簡稱CSP)的基礎(chǔ)上引入了微分方程以描述混成系統(tǒng)中的連續(xù)行為和控制邏輯,可以方便而高效地對大型控制系統(tǒng),尤其是在有通信事件發(fā)生時的情形進(jìn)行形式化建模.用HCSP建模多機器人的路徑控制算法,并用定理證明工具HProver進(jìn)行形式化驗證,結(jié)果表明,在滿足一定的初始條件下,機器人團(tuán)隊在整個運行途中不會發(fā)生碰撞.
[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.
【作者單位】： 計算機科學(xué)國家重點實驗室(中國科學(xué)院軟件研究所);
【基金】：國家自然科學(xué)基金(91118007,6110006,61304185)~~
【分類號】：TP311

【參考文獻(xiàn)】

相關(guān)期刊論文 前1條

1 郭丹青;呂繼東;王淑靈;唐濤;詹乃軍;周達(dá)天;鄒亮;;中國高速鐵路列控系統(tǒng)的形式化分析與驗證[J];中國科學(xué):信息科學(xué);2015年03期

【共引文獻(xiàn)】

相關(guān)期刊論文 前2條

1 劉濤;王淑靈;詹乃軍;;多機器人路徑規(guī)劃的安全性驗證[J];軟件學(xué)報;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期

【二級參考文獻(xiàn)】

相關(guān)期刊論文 前2條

1 徐田華;趙紅禮;唐濤;;基于有色Petri網(wǎng)的ETCS無線通信可靠性分析[J];鐵道學(xué)報;2008年01期

2 唐濤,郜春海;ETCS系統(tǒng)分析及CTCS的研究[J];機車電傳動;2004年06期

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

1 李浪;李仁發(fā);李肯立;姚鳳娟;;混成系統(tǒng)研究綜述[J];計算機應(yīng)用研究;2008年08期

2 侯建民,鄭滔,樊曉聰,李宣東,鄭國梁;線性混成系統(tǒng)的參數(shù)分析[J];計算機學(xué)報;1999年06期

3 范雙南;;基于時間序列分析的混成系統(tǒng)可靠性評價方法[J];福建電腦;2011年03期

4 鄒進(jìn);林望;羅勇;曾振柄;;基于多面體包含的非線性混成系統(tǒng)可達(dá)性分析[J];計算機應(yīng)用;2013年05期

5 卜磊;解定寶;;混成系統(tǒng)形式化驗證[J];軟件學(xué)報;2014年02期

6 喬磊;齊驥;龔育昌;;一種支持可重構(gòu)混成系統(tǒng)的操作系統(tǒng)設(shè)計與實現(xiàn)[J];計算機學(xué)報;2009年05期

7 趙劍;歐陽丹彤;王曉宇;張立明;;混成系統(tǒng)的分布式診斷方法[J];吉林大學(xué)學(xué)報(工學(xué)版);2012年06期

8 肖娟;;混成系統(tǒng)的形式驗證[J];長沙通信職業(yè)技術(shù)學(xué)院學(xué)報;2008年01期

9 葉林;湯瀑;郭立鵬;張亮;;基于混成系統(tǒng)的物聯(lián)網(wǎng)服務(wù)建模與驗證[J];小型微型計算機系統(tǒng);2013年12期

10 閻安,唐稚松;基于 XYZ/ E的混成系統(tǒng)(英文)[J];軟件學(xué)報;2000年01期

相關(guān)會議論文 前1條

1 任雁;田婕;孫輝;周永;;混成系統(tǒng)測試研究綜述[A];2011年通信與信息技術(shù)新進(jìn)展——第八屆中國通信學(xué)會學(xué)術(shù)年會論文集[C];2011年

相關(guān)博士學(xué)位論文 前6條

1 解定寶;混成系統(tǒng)有界模型檢驗優(yōu)化技術(shù)研究[D];南京大學(xué);2016年

2 王國濱;信息物理融合系統(tǒng)安全性驗證研究[D];華東師范大學(xué);2016年

3 林望;基于符號數(shù)值混合計算的混成系統(tǒng)可信分析與驗證研究[D];華東師范大學(xué);2013年

4 趙劍;混成系統(tǒng)基于模型診斷的若干問題研究[D];吉林大學(xué);2012年

5 孔輝;基于歸納不變式的混成系統(tǒng)安全性驗證[D];清華大學(xué);2013年

6 李廣元;LTLC：面向?qū)崟r與混成系統(tǒng)的連續(xù)時序邏輯[D];中國科學(xué)院軟件研究所;2001年

相關(guān)碩士學(xué)位論文 前7條

1 楊陽;基于深度優(yōu)先搜索的混成系統(tǒng)有界可達(dá)性分析[D];南京大學(xué);2013年

2 蔣慧;基于遷移系統(tǒng)語義的線性混成系統(tǒng)分析[D];南京大學(xué);2013年

3 李國拯;基于組合形式規(guī)范的混成系統(tǒng)形式化驗證方法研究[D];南京航空航天大學(xué);2015年

4 鄒進(jìn);非線性混成系統(tǒng)的可達(dá)性分析[D];溫州大學(xué);2013年

5 李倩;基于形式化方法的混成系統(tǒng)安全性檢驗[D];華東師范大學(xué);2015年

6 錢宇清;Hybrid AADL：混成系統(tǒng)體系結(jié)構(gòu)分析與設(shè)計語言[D];華東師范大學(xué);2014年

7 錢磊;信息物理融合系統(tǒng)的形式化建模與討論[D];華東師范大學(xué);2013年

，

本文編號：1534003