基于模型檢測的時空性能分析若干問題研究.pdf

1、模型檢測作為一種形式化的自動驗(yàn)證技術(shù)，可在設(shè)計和開發(fā)過程對系統(tǒng)的功能和性能進(jìn)行分析與驗(yàn)證，從而保證系統(tǒng)在運(yùn)行過程中的正確性及可靠性。然而由于系統(tǒng)的復(fù)雜性及驗(yàn)證屬性的多樣性，模型檢測的相關(guān)理論與技術(shù)還有待發(fā)展與完善。本文主要針對隨機(jī)模型檢測中的時空性能分析所涉及的一些重要內(nèi)容進(jìn)行研究，主要包括以下幾個方面:
　　(1)給出Markov決策過程模型中不確定性解決策略的定義及分類方法;分析不同策略下時空有界可達(dá)概率問題，證明在時間無關(guān)策

2、略下基于確定性選取動作和隨機(jī)選取動作的時空有界可達(dá)概率的一致性，并且論證了時間依賴策略相對于時間無關(guān)策略具有更好的時空有界可達(dá)概率。
　　(2)針對當(dāng)前連續(xù)時間Markov回報過程(Continue Time Markov RewardDecision Process，CMRDP)驗(yàn)證中只考慮狀態(tài)回報的問題，提出帶動作回報的驗(yàn)證方法?？紤]添加了動作回報的空間性能約束，擴(kuò)展現(xiàn)有的基于狀態(tài)回報的連續(xù)時間Markov回報過程，用正則表達(dá)

3、式表示驗(yàn)證屬性的路徑規(guī)范，擴(kuò)展已有路徑算子的表達(dá)能力。給出帶動作回報CMRDP和路徑規(guī)范的積模型，求解積模型在確定性策略下的誘導(dǎo)Markov回報模型(Markov Reward Model，MRM)，將CMRDP上的時空性能驗(yàn)證轉(zhuǎn)換為MRM模型上的時空可達(dá)概率分析，并給出MRM中求解可達(dá)概率的算法。
　　(3)分析連續(xù)時間Markov決策過程下的關(guān)系，在強(qiáng)互模擬關(guān)系的基礎(chǔ)上，定義弱互模擬等價關(guān)系及強(qiáng)（弱）模擬關(guān)系，證明了這些關(guān)系之

4、間內(nèi)在的聯(lián)系，同時研究了互模擬關(guān)系下的邏輯保持問題，闡述了強(qiáng)互模擬等價與asCSL(actionand state base CSL)邏輯等價性的關(guān)系，證明了弱互模擬等價與CSL(ContinuousStochastic Logic)邏輯等價性的聯(lián)系。
　　(4)采用排隊(duì)系統(tǒng)構(gòu)建云計算平臺的隨機(jī)模型，闡述云計算系統(tǒng)能耗與調(diào)度概率之間的關(guān)聯(lián)關(guān)系，以降低系統(tǒng)能耗為目標(biāo)，提出基于遺傳算法的調(diào)度概率優(yōu)化算法。然后應(yīng)用隨機(jī)模型檢測技術(shù)將計算

5、節(jié)點(diǎn)的DPM(Dynamic PowerManagement)模型建模為連續(xù)時間Markov回報模型，并使用概率模型檢測工具PRISM對節(jié)點(diǎn)能耗進(jìn)行分析。
　　(5)研究具有混合特征的混合Petri網(wǎng)和流體隨機(jī)Petri網(wǎng)，分析其內(nèi)在的建模機(jī)制。提出了一種一階混合Petri網(wǎng)轉(zhuǎn)換成流體隨機(jī)Petri網(wǎng)的形式化方法，并指出轉(zhuǎn)換得到的流體隨機(jī)Petri網(wǎng)可以對部分變遷進(jìn)行合并以減少模型的復(fù)雜度，給出變遷合并的算法，證明了轉(zhuǎn)換和合并方法