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

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

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