基于進(jìn)程代數(shù)和模型檢驗(yàn)的系統(tǒng)建模與評價.pdf

1、性能評價的目的是描述和分析系統(tǒng)的動態(tài)及與時間有關(guān)的行為。盡早將功能、時序行為檢驗(yàn)與設(shè)計相結(jié)合，可以在很大程度上消除不必要的錯誤，提高設(shè)計質(zhì)量。評價模型常采用變遷模型描述系統(tǒng)的動態(tài)行為。在實(shí)時系統(tǒng)性能(包括可靠性)的分析中，連續(xù)時間馬爾可夫鏈模型被得到廣泛應(yīng)用。但目前軟件系統(tǒng)和硬件系統(tǒng)的規(guī)模和復(fù)雜度增長迅速，企圖直接獲得系統(tǒng)的馬爾可夫模型極為繁瑣且易出錯，這就需要一種合適的建模技術(shù)，能形式化地描述系統(tǒng)且易獲得系統(tǒng)的馬爾可夫模型。而進(jìn)程代數(shù)

2、面向行為，提供了結(jié)構(gòu)化操作語義，可借助自動推理展開狀態(tài)空間，無需直接面對狀態(tài)，同時具有很自然的合成和抽象的能力，能有效壓縮狀態(tài)空間，更可將進(jìn)程代數(shù)模型映射到帶標(biāo)號的變遷系統(tǒng)，從而可方便地獲得馬爾可夫模型，因此進(jìn)程代數(shù)成為復(fù)雜系統(tǒng)性能評價的建模利器。 在進(jìn)行性能評價時，獲取如失效時間、系統(tǒng)吞吐量和利用率等性能指標(biāo)是一件很棘手的工作，且基本上是非形式化的、非專用的方法，因此通常只有一些基于狀態(tài)的度量相對簡單一點(diǎn)?；跁r序邏輯的模型檢

3、驗(yàn)可以很好地解決這個問題。模型檢驗(yàn)是一種自動驗(yàn)證方法，避免建立復(fù)雜的證明過程，并在規(guī)格說明不滿足系統(tǒng)模型的要求時能提供反例。目前很多實(shí)時系統(tǒng)性能評價的工作基于連續(xù)時間馬爾可夫鏈，直接分析實(shí)時系統(tǒng)獲得性能參數(shù)是非常困難的事情，因此需要在建模和性能評價之間搭建一個橋梁，能很好地結(jié)合實(shí)時系統(tǒng)的形式化建模和實(shí)時系統(tǒng)的性能評價分析這兩種技術(shù)，降低性能評價復(fù)雜度，提高效率。將進(jìn)程代數(shù)與模型檢驗(yàn)相結(jié)合，可以解決傳統(tǒng)性能評價工作中若干難點(diǎn)，例如：建模困

4、難且易出錯，描述不規(guī)范，缺乏合成和抽象的能力，難以進(jìn)行基于路徑的度量等等，本文就并發(fā)系統(tǒng)的進(jìn)程代數(shù)建模與實(shí)時隨機(jī)系統(tǒng)的模型檢驗(yàn)作了一定的研究。 ⑴使用進(jìn)程代數(shù)描述了Ada會合機(jī)制，Ada保護(hù)對象及Java多線程機(jī)制，并提出了一種基于進(jìn)程代數(shù)的Ada并發(fā)程序靜態(tài)死鎖檢測方法。文中詳細(xì)分析了會合通信，在每條導(dǎo)向同步的控制邊附加一個代理同步通信過程的通信原子動作，從而構(gòu)造了進(jìn)程代數(shù)會合機(jī)制模型。再根據(jù)會合通信進(jìn)程代數(shù)模型原理對源程序逐

5、層掃描，提出了一種新的掃描源程序的層操作算法，實(shí)現(xiàn)了Ada并發(fā)程序到進(jìn)程代數(shù)形式化描述的轉(zhuǎn)換，并在轉(zhuǎn)換過程中，通過進(jìn)程代數(shù)的自動等價推導(dǎo)代數(shù)表達(dá)式以模擬運(yùn)行，找出系統(tǒng)中可能觸發(fā)死鎖的死通信，進(jìn)一步結(jié)合控制依賴分析死通信的各類組合情況，檢測出潛在的死鎖環(huán)路。這種Ada并發(fā)程序的靜態(tài)死鎖檢測方法的最大優(yōu)勢是能利用進(jìn)程代數(shù)的形式化建模和自動等價推理，并在需要時通過合成和抽象降低狀態(tài)空間。由于進(jìn)程代數(shù)具有很強(qiáng)的處理抽象、過程合成及隱藏內(nèi)部細(xì)節(jié)的

6、能力，因此以進(jìn)程代數(shù)形式化系統(tǒng)為基礎(chǔ)，可支持我們在可達(dá)性分析、依賴性分析、通信關(guān)系分析、切片分析及控制流分析等領(lǐng)域的研究。 ⑵提出一種帶動作標(biāo)號的隨機(jī)變遷系統(tǒng)ALSTS(Action Labeled Stochastic Transition System)及其擴(kuò)展ALSTS<'*>，并對ALSTS<'*>系統(tǒng)進(jìn)行隨機(jī)進(jìn)程代數(shù)建模與隱馬爾可夫模型分析應(yīng)用。文中提出的帶動作標(biāo)號的隨機(jī)變遷系統(tǒng)(ALSTS)包含動作和隨機(jī)時間信息，可

7、用于表達(dá)系統(tǒng)的變遷行為、時序信息、概率特征及隨機(jī)性，ALSTS的每個狀態(tài)可對應(yīng)連續(xù)時間馬爾可夫鏈(CTMC)的一個節(jié)點(diǎn)，狀態(tài)之間的變遷對應(yīng)CTMC節(jié)點(diǎn)之間的弧，從而可獲得用于性能評價的轉(zhuǎn)換速率矩陣。由于系統(tǒng)往往會因各種缺陷或誤差等而失效，因此將ALSTS系統(tǒng)擴(kuò)展為ALSTS<'*>系統(tǒng)，允許狀態(tài)內(nèi)原子命題服從一定的概率分布，使得系統(tǒng)包含雙重隨機(jī)特性。隨后使用隨機(jī)進(jìn)程代數(shù)對ALSTS<'*>系統(tǒng)進(jìn)行了建模。本文還依據(jù)ALSTS<'*>系統(tǒng)

8、的概率特性和隨機(jī)性進(jìn)行了隱馬爾可夫模型的分析，提供的隨機(jī)分析參考可輔助測試人員對實(shí)時系統(tǒng)進(jìn)行黑盒觀測，例如，在設(shè)計測試用例時，根據(jù)若干次觀測，可以估得該測試用例對路徑的覆蓋率，進(jìn)而調(diào)整測試用例，修正覆蓋率，對重點(diǎn)模塊增強(qiáng)覆蓋；也可根據(jù)若干次觀測，估得下一次系統(tǒng)最可能的執(zhí)行路徑，從而能加快調(diào)試定位。正因?yàn)榻⒘诉@樣的隱馬爾可夫模型，使得很多分析測試成為可能或更為便捷。且對于非常復(fù)雜的黑盒系統(tǒng)，可以結(jié)合進(jìn)程代數(shù)的合成能力采用逐步分解的方法來

9、進(jìn)行觀測分析。 ⑶提出了一種基于跡的連續(xù)隨機(jī)時序邏輯tCSL(Trace based Continous Stochastic Logic)，并給出了ALSTS<'*>系統(tǒng)從隨機(jī)進(jìn)程代數(shù)建模到tCSL模型檢驗(yàn)的性能評價方法。CSL(Continuous Stochastic Logic)時序邏輯不含動作的概念，因此無法針對變遷動作進(jìn)行分析，aCSL(action labeled Continuous Stochastic Log

10、ic)雖然可以分析變遷過程中的動作，但不能分析動作的執(zhí)行順序，本文在CSL和aCSL的基礎(chǔ)上增加了動作的概念、關(guān)鍵路徑的概念及跡關(guān)鍵動作的概念，描述了tCSL的詞法和語義，對不限時與限時的“Next”和“Umil”時序操作給出了基于關(guān)鍵路徑和關(guān)鍵動作的穩(wěn)態(tài)概率分析，重點(diǎn)闡述了針對路徑的tCSL模型檢驗(yàn)的方法，并通過實(shí)例分析，結(jié)合ALSTS<'*>系統(tǒng)的隨機(jī)進(jìn)程代數(shù)建模，實(shí)現(xiàn)了對關(guān)鍵動作序列有要求的路徑相關(guān)的系統(tǒng)性能評價。并給出了tCSL