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

【文章來(lái)源】：華東師范大學(xué)上海市 211工程院校 985工程院校 教育部直屬院校

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

【學(xué)位級(jí)別】：博士

【部分圖文】：

模型檢測(cè)的流程

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

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

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



本文編號(hào)：3568329