本文關(guān)鍵詞：面向航電系統(tǒng)的形式化建模與驗證

  更多相關(guān)文章： AADL 數(shù)據(jù)約束 連續(xù)時間 ZIA DT-PZIA 模型檢測

【摘要】：結(jié)構(gòu)分析和設計語言(architecture analysis and design language)是嵌入式實時系統(tǒng)的一種體系結(jié)構(gòu)描述語言標準,廣泛應用于航空宇航工業(yè)中對安全關(guān)鍵應用系統(tǒng)的建模。確保建模的正確性及其可靠性成為當前AADL研究的一大熱點領(lǐng)域。AADL在建模過程中對線程、進程、行為附件、連接等進行了一定的語義描述,但對于模型中的狀態(tài)及狀態(tài)變遷的數(shù)據(jù)約束性質(zhì)的描述略顯不足,而形式規(guī)格說明語言Z語言在數(shù)據(jù)約束的描述方面具有顯著的作用,通過對AADL進行Z語言擴充,使得建立的模型可以更好的轉(zhuǎn)換為形式化模型,從而使得模型檢測這一形式化驗證技術(shù)可用于轉(zhuǎn)換后的模型。模型檢測方法作為一種嚴格的以數(shù)學為基礎的驗證技術(shù),能夠精確、抽象、簡明地規(guī)范和驗證軟件系統(tǒng)及其性質(zhì),有效的確保軟件的安全性和可靠性。本文在AADL的基礎上擴展Z,提出了Z-AADL規(guī)范,即將Z形式規(guī)格說明語言與AADL規(guī)范相結(jié)合形成一種可以描述帶數(shù)據(jù)約束實時系統(tǒng)的形式化規(guī)范—Z-AADL。然后,提出一種描述帶數(shù)據(jù)約束實時系統(tǒng)的形式化規(guī)范?基于連續(xù)時間的ZIA規(guī)范,并將Z-AADL轉(zhuǎn)換為基于連續(xù)時間的ZIA規(guī)范模型,這樣在實現(xiàn)了對基于連續(xù)時間的ZIA模型的模型檢測的同時,其實質(zhì)上就是對Z-AADL的模型檢測。本文給出了一種模型檢測算法,適用于連續(xù)時間的ZIA模型,并通過一個實例驗證,詳細的闡述了文章方法的可行性和有效性。另外,一般意義的ZIA缺乏刻畫系統(tǒng)概率約束方面的能力,鑒于此,文章在傳統(tǒng)的ZIA上擴展了概率性質(zhì)提出一種基于離散時間的概率ZIA規(guī)范?DT-PZIA,彌補了傳統(tǒng)ZIA只能夠刻畫系統(tǒng)中的行為和狀態(tài),而不能刻畫概率性質(zhì)的缺陷。為了解決航電系統(tǒng)中的一個子系統(tǒng),即概率系統(tǒng)中的概率約束問題,本文還介紹了一個用于表達系統(tǒng)中性質(zhì)的具體度量值的形式化語言,與傳統(tǒng)的時序邏輯相比,這種邏輯不僅可以表達系統(tǒng)的時序性質(zhì),而且可以表達系統(tǒng)的度量性質(zhì)。最后本文同樣給出了檢測算法,其適用于離散時間的概率系統(tǒng)的模型檢測,并給出了實例以證明方法的可行性。
【學位授予單位】：南京航空航天大學
【學位級別】：碩士
【學位授予年份】：2016
【分類號】：V243

【相似文獻】

中國期刊全文數(shù)據(jù)庫 前10條

1 王遠達;宋筆鋒;姬東朝;史彥斌;;軍機航電系統(tǒng)實現(xiàn)兩級維修的關(guān)鍵技術(shù)[J];火力與指揮控制;2009年08期

2 蔣國峰;扈勝超;;航電系統(tǒng)外場保障實習臺的設計與研究[J];航空計算技術(shù);2010年05期

3 張U，

本文編號：1278437