基于模型檢測(cè)的時(shí)空性能分析若干問題研究
發(fā)布時(shí)間：2018-07-16 09:18
【摘要】：模型檢測(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)策略下基于確定性選取動(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 Reward Decision 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á)式表示驗(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)系之間內(nèi)在的聯(lián)系,同時(shí)研究了互模擬關(guān)系下的邏輯保持問題,闡述了強(qiáng)互模擬等價(jià)與asCSL(action and state base CSL)邏輯等價(jià)性的關(guān)系,證明了弱互模擬等價(jià)與CSL (Continuous Stochastic 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ì)算節(jié)點(diǎn)的DPM (Dynamic Power Management)模型建模為連續(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)換和合并方法的正確性。闡述了流體隨機(jī)Petri網(wǎng)模型下基于擴(kuò)展CSL時(shí)態(tài)邏輯的模型檢測(cè)方法。
[Abstract]:As a formal automatic verification technology, model checking can analyze and verify the function and performance of the system in the design and development process, so as to ensure the correctness and reliability of the system in the running process. However, due to the complexity of the system and the diversity of verification attributes, the theory and technology of model checking need to be developed and improved. In this paper, some important contents of spatio-temporal performance analysis in stochastic model detection are studied, including the following aspects: (1) the definition and classification method of uncertainty resolution strategy in Markov decision process model are given; By analyzing the bounded reachability of time and space under different strategies, we prove the consistency of the bounded probability of time and space based on deterministic and random selected actions in time independent strategies. And it is proved that the time-dependent strategy has better spatio-temporal bounded reachability than time-independent strategy. (2) considering the problem of state return only in the verification of continuous time Markov return process (CMRDP), A verification method with action return is proposed. Considering the spatial performance constraints of action returns, the existing continuous-time Markov return processes based on state returns are extended, the path specification for verifying attributes is represented by regular expressions, and the expression ability of existing path operators is extended. The product model with action return CMRDP and path specification is given, and the induced Markov return model (MRM) of product model under deterministic strategy is solved. The spatio-temporal performance verification on CMRDP is transformed into the analysis of time-space reachability probability on MRM model. An algorithm for solving reachable probability in MRM is given. (3) the relations under continuous time Markov decision process are analyzed. On the basis of strong mutual simulation relation, the equivalent relation and strong (weak) simulation relation are defined. In this paper, we prove the internal relation between these relations, study the problem of logic preservation under the mutual simulation relation, and expound the relation between strong mutual simulation equivalence and asCSL (action and state base logic equivalence. It is proved that the relation between the weak mutual simulation equivalence and the logical equivalence of CSL (continuous Stochastic Logic). (4) the stochastic model of cloud computing platform is constructed by queueing system, and the relationship between the energy consumption and scheduling probability of cloud computing system is expounded, with the aim of reducing the energy consumption of cloud computing system. A scheduling probability optimization algorithm based on genetic algorithm is proposed. Then the DPM (dynamic Power Management) model of computing nodes is modeled as a continuous-time Markov return model using random model detection technology. The probabilistic model checking tool PRISM is used to analyze node energy consumption. (5) Hybrid Petri nets and fluid stochastic Petri nets with mixed characteristics are studied and their intrinsic modeling mechanisms are analyzed. In this paper, a formal method of converting first-order hybrid Petri nets into fluid stochastic Petri nets is proposed. It is pointed out that the transformed fluid stochastic Petri nets can merge some transitions to reduce the complexity of the model, and the algorithm of transition merging is given. The correctness of the conversion and merging methods is proved. A model detection method based on extended CSL temporal logic for fluid stochastic Petri net model is presented.
【學(xué)位授予單位】：合肥工業(yè)大學(xué)
【學(xué)位級(jí)別】：博士
【學(xué)位授予年份】：2016
【分類號(hào)】：O211.62;TP301.1
[Abstract]:As a formal automatic verification technology, model checking can analyze and verify the function and performance of the system in the design and development process, so as to ensure the correctness and reliability of the system in the running process. However, due to the complexity of the system and the diversity of verification attributes, the theory and technology of model checking need to be developed and improved. In this paper, some important contents of spatio-temporal performance analysis in stochastic model detection are studied, including the following aspects: (1) the definition and classification method of uncertainty resolution strategy in Markov decision process model are given; By analyzing the bounded reachability of time and space under different strategies, we prove the consistency of the bounded probability of time and space based on deterministic and random selected actions in time independent strategies. And it is proved that the time-dependent strategy has better spatio-temporal bounded reachability than time-independent strategy. (2) considering the problem of state return only in the verification of continuous time Markov return process (CMRDP), A verification method with action return is proposed. Considering the spatial performance constraints of action returns, the existing continuous-time Markov return processes based on state returns are extended, the path specification for verifying attributes is represented by regular expressions, and the expression ability of existing path operators is extended. The product model with action return CMRDP and path specification is given, and the induced Markov return model (MRM) of product model under deterministic strategy is solved. The spatio-temporal performance verification on CMRDP is transformed into the analysis of time-space reachability probability on MRM model. An algorithm for solving reachable probability in MRM is given. (3) the relations under continuous time Markov decision process are analyzed. On the basis of strong mutual simulation relation, the equivalent relation and strong (weak) simulation relation are defined. In this paper, we prove the internal relation between these relations, study the problem of logic preservation under the mutual simulation relation, and expound the relation between strong mutual simulation equivalence and asCSL (action and state base logic equivalence. It is proved that the relation between the weak mutual simulation equivalence and the logical equivalence of CSL (continuous Stochastic Logic). (4) the stochastic model of cloud computing platform is constructed by queueing system, and the relationship between the energy consumption and scheduling probability of cloud computing system is expounded, with the aim of reducing the energy consumption of cloud computing system. A scheduling probability optimization algorithm based on genetic algorithm is proposed. Then the DPM (dynamic Power Management) model of computing nodes is modeled as a continuous-time Markov return model using random model detection technology. The probabilistic model checking tool PRISM is used to analyze node energy consumption. (5) Hybrid Petri nets and fluid stochastic Petri nets with mixed characteristics are studied and their intrinsic modeling mechanisms are analyzed. In this paper, a formal method of converting first-order hybrid Petri nets into fluid stochastic Petri nets is proposed. It is pointed out that the transformed fluid stochastic Petri nets can merge some transitions to reduce the complexity of the model, and the algorithm of transition merging is given. The correctness of the conversion and merging methods is proved. A model detection method based on extended CSL temporal logic for fluid stochastic Petri net model is presented.
【學(xué)位授予單位】：合肥工業(yè)大學(xué)
【學(xué)位級(jí)別】：博士
【學(xué)位授予年份】：2016
【分類號(hào)】：O211.62;TP301.1
【相似文獻(xiàn)】
相關(guān)期刊論文 前10條
1 陳清亮;朱可宜;;多智能體協(xié)同的認(rèn)知規(guī)范模型檢測(cè)算法[J];中山大學(xué)學(xué)報(bào)(自然科學(xué)版);2009年01期
2 周從華;邢支虎;劉志鋒;王昌達(dá);;馬爾可夫決策過程的限界模型檢測(cè)[J];計(jì)算機(jī)學(xué)報(bào);2013年12期
3 吉猛;胡克瑾;;基于模型檢測(cè)的電子商務(wù)鑒證技術(shù)[J];陜西師范大學(xué)學(xué)報(bào)(自然科學(xué)版);2006年04期
4 寧正元;胡山立;賴賢偉;;交互時(shí)態(tài)信念邏輯及其模型檢測(cè)[J];南京大學(xué)學(xué)報(bào)(自然科學(xué)版);2008年02期
5 王曦;徐中偉;梅萌;;基于模型檢測(cè)的軟件安全性驗(yàn)證方法[J];武漢大學(xué)學(xué)報(bào)(理學(xué)版);2010年02期
6 王晶;張廣泉;;基于概率時(shí)間自動(dòng)機(jī)的模型檢測(cè)反例表示研究[J];蘇州大學(xué)學(xué)報(bào)(自然科學(xué)版);2011年02期
7 高妍妍;李曦;周學(xué)海;;L4進(jìn)程間通信機(jī)制的模型檢測(cè)方法[J];中國科學(xué)院研究生院學(xué)報(bào);2011年06期
8 王扣武;張s，
本文編號(hào)：2125934
本文鏈接：http://www.sikaile.net/shoufeilunwen/xxkjbs/2125934.html
最近更新
教材專著
