基于模型檢測(cè)的時(shí)空性能分析若干問題研究
[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