隨著實時系統(tǒng)使用范圍的日益擴大,對實時系統(tǒng)的可靠性的要求也越來越高。對實時系統(tǒng)的功能、性能和可靠性進行的評估已成為一個重要的研究課題。作為提高軟件可信度的重要手段,概率模型檢測可以自動化地對軟件及硬件系統(tǒng)完成形式化驗證,從定量的角度給出其屬性的分析結(jié)果。本文的主要工作就是研究對實時系統(tǒng)實施概率模型檢測的理論框架,提出對實時系統(tǒng)進行概率模型檢測的解決方案,為概率模型檢測技術(shù)進一步走向應用進行探索。由于實時系統(tǒng)其自身的特殊性,對實時系統(tǒng)進行概率模型檢測是十分困難的。歸納起來,實時系統(tǒng)具有以下三個特性:實時性,自穩(wěn)定性和交互性。第一,由于實時系統(tǒng)具有實時響應的特性,實時系統(tǒng)模型的行為往往是隨時間連續(xù)變化的。這種模型的根本特征是其狀態(tài)空間是無限的。但是概率模型檢測技術(shù)只適用于有限狀態(tài)空間模型,因此,對實時系統(tǒng)實施概率模型檢測幾乎是不可能的。第二,實時系統(tǒng)具有自穩(wěn)定的特性,即在無需外界干預的情況下,實時系統(tǒng)可以自動地從一個不穩(wěn)定狀態(tài)到達另一個穩(wěn)定狀態(tài)。支配實時系統(tǒng)自穩(wěn)定過程的自穩(wěn)定算法的性能成為制約實時系統(tǒng)的性能的關(guān)鍵因素。第三,實時系統(tǒng)要和工作環(huán)境或用戶進行交互。對實時系統(tǒng)的性能、可靠性的評估... 

【文章來源】：華東師范大學上海市 211工程院校 985工程院校 教育部直屬院校

【文章頁數(shù)】：164 頁

【學位級別】：博士

【部分圖文】：

模型檢測的流程

圖 2. 1 一個 DTMC D.1中的 DTMC M，其遷移關(guān)系可以用遷移概率矩陣P= 的模型檢測屬性規(guī)約可以用概率計算樹邏輯(Probabilistic C)[24]描述，它是時序邏輯 CTL 的概率擴展。CTL 語法). PCTL語法如下： | a | /\ | | P~p[ ]

圖 2. 2 確定 Prs( a U b)的概率 DTMC 附加成本/收益MC 也可以增加成本/收益計算。對于 DTMC，成本/收益可以), 其中 ρ,ι 分別代表狀態(tài)成本（收益）和遷移成本（收益）。ρ(s)指 DTMC 處于狀態(tài) s 時所消耗的成本（獲得的收益）。可以由成本（收益）函數(shù) ρ：S R+賦值給狀態(tài)。遷移成本 DTMC 從狀態(tài) s 遷移到 積累的成本（收益）。遷移成本（收收益）函數(shù) ι：S S R+賦值給遷移。/收益用來附帶資源使用情況信息，如能量消耗或者丟失的分過對 DTMC 加批注的方式來表示。成本/收益可以有兩種形的。對于一個 DTMC D =｛S,sinit,P,AP,L｝，成本是兩個函數(shù)構(gòu)

【參考文獻】：
期刊論文
[1]馬爾可夫決策過程的限界模型檢測[J]. 周從華,邢支虎,劉志鋒,王昌達.  計算機學報. 2013(12)
[2]可信計算的研究與發(fā)展[J]. 沈昌祥,張煥國,王懷民,王戟,趙波,嚴飛,余發(fā)江,張立強,徐明迪.  中國科學:信息科學. 2010(02)
[3]高可信軟件工程技術(shù)[J]. 陳火旺,王戟,董威.  電子學報. 2003(S1)



本文編號：3568329