無人駕駛汽車決策系統(tǒng)的規(guī)則正確性驗(yàn)證.pdf

1、隨著信息技術(shù)的發(fā)展，無人駕駛車輛技術(shù)日漸成為科學(xué)研究的重點(diǎn)領(lǐng)域之一，各國都在其中投入了大量的人力物力。無人駕駛車輛技術(shù)能夠?qū)⑷祟愸{駛員從枯燥危險的駕駛工作中解放出來，減少了車輛行為的隨機(jī)性，使車輛的行為變得可預(yù)測，可以極大地提高車輛行駛的穩(wěn)定性。另外，無人駕駛車輛技術(shù)提高了車輛對環(huán)境的反應(yīng)速度，增強(qiáng)了車輛的安全性，也可以大大縮短行車間距，從而增加公路的運(yùn)輸能力。同時，無人駕駛車輛技術(shù)改善了車輛對環(huán)境的感知精度，消除了因駕駛員個人問題而造

2、成的交通事故。
　　無人駕駛車輛技術(shù)的核心在于其決策系統(tǒng)的開發(fā)，當(dāng)前無人車決策系統(tǒng)開發(fā)過程中面臨著諸多難題，主要包括以下幾點(diǎn)：由人工編寫的代碼成本高且維護(hù)困難；決策規(guī)則與系統(tǒng)軟件沒有實(shí)現(xiàn)分離；設(shè)計過程中可能存在潛在的缺陷和錯誤；軟件開發(fā)與安全檢查不同步。
　　針對以上問題，課題組提出了驗(yàn)證驅(qū)動的基于代碼自動生成的無人車決策系統(tǒng)開發(fā)框架。課題組早期的工作包括設(shè)計了描述無人車決策規(guī)則的中間語言，并設(shè)計實(shí)現(xiàn)了無人車決策系統(tǒng)輔助開發(fā)

3、工具，解決了開發(fā)過程中的前兩個難題。
　　為了解決無人車決策系統(tǒng)中的安全性問題，本文在代碼自動生成技術(shù)的基礎(chǔ)上引入了模型檢驗(yàn)技術(shù)，自動生成無人車的模型代碼，并對無人車決策系統(tǒng)進(jìn)行環(huán)境建模，通過形式化驗(yàn)證可以發(fā)現(xiàn)無人車決策系統(tǒng)設(shè)計過程中不易察覺的缺陷和錯誤，解決其安全性不足的問題，同時能夠?qū)踩珯z查與軟件開發(fā)過程同步，降低其維護(hù)成本?；谠摽蚣?，本文將模型檢驗(yàn)?zāi)K集成到已有的無人車決策系統(tǒng)輔助開發(fā)工具 UNMANNED_RULE_E