面向混成系統(tǒng)的ZIA形式化模型及其自動(dòng)驗(yàn)證方法研究.pdf

1、目前,嵌入式實(shí)時(shí)系統(tǒng)的廣泛應(yīng)用使得確保其正確性和可靠性成為當(dāng)前的研究熱點(diǎn)。MARTE(Modeling and Analysis of Real Time and Embedded systems)是UML在嵌入式實(shí)時(shí)系統(tǒng)領(lǐng)域的建模規(guī)范,彌補(bǔ)了UML對嵌入式實(shí)時(shí)系統(tǒng)領(lǐng)域非功能屬性表達(dá)能力的不足。MARTE規(guī)范采用圖形化的方式描述系統(tǒng),缺乏精確的語義,因此難以直接進(jìn)行形式化分析和驗(yàn)證。在現(xiàn)代軟件系統(tǒng)開發(fā)過程當(dāng)中,還經(jīng)常會(huì)要求在某些限定的時(shí)

2、間約束之下,對系統(tǒng)的輸入數(shù)據(jù)以及系統(tǒng)內(nèi)部狀態(tài)之間的變遷進(jìn)行相應(yīng)的處理,最后給出對應(yīng)的輸出數(shù)據(jù),因此對數(shù)據(jù)變量進(jìn)行處理也十分必要。形式化方法作為一種以數(shù)學(xué)為基礎(chǔ)的方法,能夠清晰、精確、抽象、簡明地規(guī)范和驗(yàn)證軟件系統(tǒng)及其性質(zhì),極大地提高軟件的安全性和可靠性。
　　本文通過將MARTE模型轉(zhuǎn)換到形式化模型進(jìn)行驗(yàn)證,以確保軟件的可信度。首先,對MARTE進(jìn)行擴(kuò)充,將MARTE與Z語言相結(jié)合提出一種描述帶有數(shù)據(jù)約束的嵌入式實(shí)時(shí)系統(tǒng)規(guī)范?Z-

3、MARTE。然后,提出一種描述帶數(shù)據(jù)約束實(shí)時(shí)系統(tǒng)的形式化規(guī)范?基于連續(xù)時(shí)間的ZIA規(guī)范,并將Z-MARTE轉(zhuǎn)換為基于連續(xù)時(shí)間的ZIA規(guī)范模型,這樣在實(shí)現(xiàn)了對基于連續(xù)時(shí)間的ZIA模型的模型檢測時(shí),也就實(shí)現(xiàn)了對Z-MARTE的模型檢測。本文最后給出基于連續(xù)時(shí)間的ZIA規(guī)范模型的模型檢測算法,并通過一個(gè)實(shí)例驗(yàn)證,闡述了文章方法的可行性和有效性。
　　另外,由于傳統(tǒng)的ZIA沒有刻畫系統(tǒng)概率方面的能力,因此文章在傳統(tǒng)的ZIA上擴(kuò)展了概率性質(zhì)