基于模型的無(wú)人機(jī)飛控系統(tǒng)建模及安全性驗(yàn)證方法研究.pdf

1、無(wú)人機(jī)飛行控制系統(tǒng)作為飛行器關(guān)鍵系統(tǒng)之一，負(fù)責(zé)飛行器從起飛至降落的整個(gè)飛行過(guò)程。飛控系統(tǒng)軟件具有安全性能要求高、功能繁多、復(fù)雜性高的特點(diǎn)，而傳統(tǒng)的軟件開發(fā)方式存在諸多不足。同時(shí)采用形式化驗(yàn)證方法對(duì)飛控系統(tǒng)軟件進(jìn)行安全性驗(yàn)證時(shí)，安全屬性的提取沒(méi)有統(tǒng)一的有效的方法；安全屬性的驗(yàn)證過(guò)中易產(chǎn)生空間爆炸問(wèn)題，研究如何對(duì)狀態(tài)空間進(jìn)行約簡(jiǎn)也是當(dāng)前所的面臨的重要任務(wù)。
　　本文采用了基于模型的軟件開發(fā)工具SCADE開發(fā)飛控系統(tǒng)軟件，同時(shí)針對(duì)飛控系

2、統(tǒng)軟件高安全可靠性的要求，研究了基于故障樹的安全屬性提取方法，并結(jié)合模型檢驗(yàn)技術(shù)，進(jìn)行安全性驗(yàn)證。針對(duì)驗(yàn)證過(guò)程中產(chǎn)生空間爆炸問(wèn)題，提出了基于切片和系統(tǒng)分解的方法對(duì)驗(yàn)證空間進(jìn)行劃分，分步驗(yàn)證。本文主要包括以下內(nèi)容：
　　首先對(duì)安全屬性提取方法及模型檢驗(yàn)技術(shù)進(jìn)行研究。介紹了基于模型的軟件開發(fā)方式，給出了故障樹的構(gòu)建準(zhǔn)則和安全屬性提取及轉(zhuǎn)化方法。然后，對(duì)狀態(tài)空間約簡(jiǎn)問(wèn)題進(jìn)行研究。針對(duì)形式化驗(yàn)證過(guò)程中出現(xiàn)的狀態(tài)空間爆炸問(wèn)題，采用了基于切片