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

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

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

【相似文獻(xiàn)】

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

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

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

3 張U，

本文編號(hào)：1278437