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

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

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

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

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

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

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

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

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

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

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