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

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

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

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