基于模型檢測(cè)的時(shí)空性能分析若干問題研究.pdf

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

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

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

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

5、節(jié)點(diǎn)的DPM(Dynamic PowerManagement)模型建模為連續(xù)時(shí)間Markov回報(bào)模型，并使用概率模型檢測(cè)工具PRISM對(duì)節(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)可以對(duì)部分變遷進(jìn)行合并以減少模型的復(fù)雜度，給出變遷合并的算法，證明了轉(zhuǎn)換和合并方法