基于模型檢測的時空性能分析若干問題研究
發(fā)布時間：2018-07-16 09:18
【摘要】：模型檢測作為一種形式化的自動驗證技術(shù),可在設(shè)計和開發(fā)過程對系統(tǒng)的功能和性能進行分析與驗證,從而保證系統(tǒng)在運行過程中的正確性及可靠性。然而由于系統(tǒng)的復(fù)雜性及驗證屬性的多樣性,模型檢測的相關(guān)理論與技術(shù)還有待發(fā)展與完善。本文主要針對隨機模型檢測中的時空性能分析所涉及的一些重要內(nèi)容進行研究,主要包括以下幾個方面：(1)給出Markov決策過程模型中不確定性解決策略的定義及分類方法；分析不同策略下時空有界可達概率問題,證明在時間無關(guān)策略下基于確定性選取動作和隨機選取動作的時空有界可達概率的一致性,并且論證了時間依賴策略相對于時間無關(guān)策略具有更好的時空有界可達概率。(2)針對當前連續(xù)時間Markov回報過程(Continue Time Markov Reward Decision Process, CMRDP)驗證中只考慮狀態(tài)回報的問題,提出帶動作回報的驗證方法�？紤]添加了動作回報的空間性能約束,擴展現(xiàn)有的基于狀態(tài)回報的連續(xù)時間Markov回報過程,用正則表達式表示驗證屬性的路徑規(guī)范,擴展已有路徑算子的表達能力。給出帶動作回報CMRDP和路徑規(guī)范的積模型,求解積模型在確定性策略下的誘導(dǎo)Markov回報模型(Markov Reward Model, MRM),將CMRDP上的時空性能驗證轉(zhuǎn)換為MRM模型上的時空可達概率分析,并給出MRM中求解可達概率的算法。(3)分析連續(xù)時間Markov決策過程下的關(guān)系,在強互模擬關(guān)系的基礎(chǔ)上,定義弱互模擬等價關(guān)系及強(弱)模擬關(guān)系,證明了這些關(guān)系之間內(nèi)在的聯(lián)系,同時研究了互模擬關(guān)系下的邏輯保持問題,闡述了強互模擬等價與asCSL(action and state base CSL)邏輯等價性的關(guān)系,證明了弱互模擬等價與CSL (Continuous Stochastic Logic)邏輯等價性的聯(lián)系。(4)采用排隊系統(tǒng)構(gòu)建云計算平臺的隨機模型,闡述云計算系統(tǒng)能耗與調(diào)度概率之間的關(guān)聯(lián)關(guān)系,以降低系統(tǒng)能耗為目標,提出基于遺傳算法的調(diào)度概率優(yōu)化算法。然后應(yīng)用隨機模型檢測技術(shù)將計算節(jié)點的DPM (Dynamic Power Management)模型建模為連續(xù)時間Markov回報模型,并使用概率模型檢測工具PRISM對節(jié)點能耗進行分析。(5)研究具有混合特征的混合Petri網(wǎng)和流體隨機Petri網(wǎng),分析其內(nèi)在的建模機制。提出了一種一階混合Petri網(wǎng)轉(zhuǎn)換成流體隨機Petri網(wǎng)的形式化方法,并指出轉(zhuǎn)換得到的流體隨機Petri網(wǎng)可以對部分變遷進行合并以減少模型的復(fù)雜度,給出變遷合并的算法,證明了轉(zhuǎn)換和合并方法的正確性。闡述了流體隨機Petri網(wǎng)模型下基于擴展CSL時態(tài)邏輯的模型檢測方法。
[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é)位級別】：博士
【學(xué)位授予年份】：2016
【分類號】：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é)位級別】：博士
【學(xué)位授予年份】：2016
【分類號】：O211.62;TP301.1
【相似文獻】
相關(guān)期刊論文 前10條
1 陳清亮;朱可宜;;多智能體協(xié)同的認知規(guī)范模型檢測算法[J];中山大學(xué)學(xué)報(自然科學(xué)版);2009年01期
2 周從華;邢支虎;劉志鋒;王昌達;;馬爾可夫決策過程的限界模型檢測[J];計算機學(xué)報;2013年12期
3 吉猛;胡克瑾;;基于模型檢測的電子商務(wù)鑒證技術(shù)[J];陜西師范大學(xué)學(xué)報(自然科學(xué)版);2006年04期
4 寧正元;胡山立;賴賢偉;;交互時態(tài)信念邏輯及其模型檢測[J];南京大學(xué)學(xué)報(自然科學(xué)版);2008年02期
5 王曦;徐中偉;梅萌;;基于模型檢測的軟件安全性驗證方法[J];武漢大學(xué)學(xué)報(理學(xué)版);2010年02期
6 王晶;張廣泉;;基于概率時間自動機的模型檢測反例表示研究[J];蘇州大學(xué)學(xué)報(自然科學(xué)版);2011年02期
7 高妍妍;李曦;周學(xué)海;;L4進程間通信機制的模型檢測方法[J];中國科學(xué)院研究生院學(xué)報;2011年06期
8 王扣武;張s，
本文編號：2125934
本文鏈接：http://www.wukwdryxk.cn/shoufeilunwen/xxkjbs/2125934.html
最近更新
教材專著
