綜合模塊化航空電子系統(tǒng)重構(gòu)與驗(yàn)證方法研究

發(fā)布時間：2020-06-18 19:06

【摘要】：為了滿足飛機(jī)日益增長的軍事和民用需求,綜合模塊化航空電子系統(tǒng)(Integrated Modular Avionics,IMA)近年來受到了工業(yè)界和學(xué)術(shù)界的廣泛關(guān)注。IMA系統(tǒng)是安全攸關(guān)的嵌入式系統(tǒng),當(dāng)運(yùn)行環(huán)境變化或組件故障時,系統(tǒng)對軟件和硬件資源進(jìn)行重構(gòu)配置,保證功能和性能要求。重構(gòu)必須嚴(yán)格遵照預(yù)先設(shè)定的策略執(zhí)行,避免出現(xiàn)失控情況,引發(fā)系統(tǒng)故障。因此,重構(gòu)設(shè)計過程中,如何對IMA系統(tǒng)資源進(jìn)行分配,確保滿足系統(tǒng)的功能性需求和安全性等質(zhì)量屬性要求,是整個飛機(jī)功能正常運(yùn)行的關(guān)鍵。目前在IMA系統(tǒng)重構(gòu)設(shè)計方面已取得了諸多研究進(jìn)展和重要成果,但現(xiàn)有方法還面臨以下挑戰(zhàn):首先,系統(tǒng)重構(gòu)是邏輯架構(gòu)到物理實(shí)現(xiàn)的重新映射,過程具有多樣性和不確定性,且缺少對系統(tǒng)資源的精確描述,收集系統(tǒng)軟件和硬件資源信息困難,重構(gòu)自動化程度不高。其次,現(xiàn)有的驗(yàn)證方法在系統(tǒng)邏輯模型、物理架構(gòu)模型、分區(qū)映射方面各有側(cè)重,但缺少必要銜接,模型之間未建立統(tǒng)一的映射關(guān)系,驗(yàn)證結(jié)果的完整性有待提高。因此,通過基于模型的重構(gòu)方法,簡化映射過程,驗(yàn)證系統(tǒng)的功能性和安全性需求,實(shí)現(xiàn)對系統(tǒng)資源的重構(gòu)配置,具有一定的研究意義和實(shí)用價值。本文圍繞基于模型的IMA系統(tǒng)重構(gòu)設(shè)計過程中建模、映射、驗(yàn)證、藍(lán)圖生成等內(nèi)容進(jìn)行詳細(xì)討論。論文的主要研究成果如下:(1)為保證重構(gòu)后系統(tǒng)邏輯架構(gòu)滿足功能性需求,提出了一種SysML活動圖的自動機(jī)模型構(gòu)建和驗(yàn)證方法。采用擴(kuò)展的有限自動機(jī)模型建�；顒訄D內(nèi)容和嵌套調(diào)用,使用線性時序邏輯表示功能性需求屬性,通過相應(yīng)的轉(zhuǎn)換算法和模型檢測方法確認(rèn)設(shè)計的功能邏輯流程與需求的一致性。提出了一種基于模型的測試用例生成方法,將確認(rèn)正確的活動圖轉(zhuǎn)為帶約束的接口自動機(jī),生成測試模型,通過其特有的樂觀方法和博弈思想組合活動間的調(diào)用關(guān)系。然后在滿足流約束條件組合覆蓋準(zhǔn)則的前提下,設(shè)計了測試用例生成算法,自動生成測試用例,用于架構(gòu)的功能性測試。(2)為保證重構(gòu)后系統(tǒng)邏輯架構(gòu)滿足安全性需求,提出了一種基于模型的系統(tǒng)安全性需求描述和驗(yàn)證方法。該方法針對系統(tǒng)功能需求、安全性目標(biāo)和失效狀態(tài),建立危害用例,提取安全性需求;采用帶功能失效的狀態(tài)機(jī)圖描述包含安全性需求的系統(tǒng)功能模型,并使用安全擴(kuò)展層次自動機(jī)作為中間狀態(tài),通過轉(zhuǎn)換算法實(shí)現(xiàn)系統(tǒng)功能模型的形式化描述,通過模型檢測方法完成安全性需求驗(yàn)證。(3)為保證重構(gòu)后系統(tǒng)物理架構(gòu)滿足安全性需求,提出了一種基于模型的組件錯誤行為描述和驗(yàn)證方法。該方法通過分析系統(tǒng)需求和安全性目標(biāo),建立物理架構(gòu)模型,采用錯誤模型附件描述組件的錯誤行為和導(dǎo)致的故障影響;使用層次自動機(jī)作為中間狀態(tài),通過轉(zhuǎn)換算法實(shí)現(xiàn)物理架構(gòu)錯誤行為模型的形式化描述,采用模型檢測驗(yàn)證故障影響是否滿足安全性需求。(4)針對系統(tǒng)重配置、重映射過程復(fù)雜,功能性和安全性需求驗(yàn)證困難的問題,提出一種基于模式的IMA系統(tǒng)重構(gòu)方法。將系統(tǒng)邏輯架構(gòu)劃分為多個層級,給出邏輯架構(gòu)模型到AADL組件,以及AADL組件到ARINC653元素的映射規(guī)則;采用模式表示系統(tǒng)運(yùn)行時資源配置,通過模式遷移實(shí)現(xiàn)不同層級的重構(gòu)設(shè)計,并對各模式下的系統(tǒng)邏輯架構(gòu)和映射所得的物理架構(gòu)模型進(jìn)行驗(yàn)證和分析;構(gòu)建系統(tǒng)藍(lán)圖生成算法,根據(jù)模式遷移和驗(yàn)證結(jié)果自動生成重構(gòu)藍(lán)圖,指導(dǎo)系統(tǒng)資源動態(tài)配置,實(shí)現(xiàn)相應(yīng)的功能。
【學(xué)位授予單位】：西北大學(xué)
【學(xué)位級別】：博士
【學(xué)位授予年份】：2019
【分類號】：V243;TP311.52
【圖文】：

驗(yàn)證結(jié)果,性質(zhì),反例,制動裝置