基于模型检测的时空性能分析若干问题研究
发布时间：2018-07-16 09:18
【摘要】：模型检测作为一种形式化的自动验证技术,可在设计和开发过程对系统的功能和性能进行分析与验证,从而保证系统在运行过程中的正确性及可靠性。然而由于系统的复杂性及验证属性的多样性,模型检测的相关理论与技术还有待发展与完善。本文主要针对随机模型检测中的时空性能分析所涉及的一些重要内容进行研究,主要包括以下几个方面：(1)给出Markov决策过程模型中不确定性解决策略的定义及分类方法；分析不同策略下时空有界可达概率问题,证明在时间无关策略下基于确定性选取动作和随机选取动作的时空有界可达概率的一致性,并且论证了时间依赖策略相对于时间无关策略具有更好的时空有界可达概率。(2)针对当前连续时间Markov回报过程(Continue Time Markov Reward Decision Process, CMRDP)验证中只考虑状态回报的问题,提出带动作回报的验证方法。考虑添加了动作回报的空间性能约束,扩展现有的基于状态回报的连续时间Markov回报过程,用正则表达式表示验证属性的路径规范,扩展已有路径算子的表达能力。给出带动作回报CMRDP和路径规范的积模型,求解积模型在确定性策略下的诱导Markov回报模型(Markov Reward Model, MRM),将CMRDP上的时空性能验证转换为MRM模型上的时空可达概率分析,并给出MRM中求解可达概率的算法。(3)分析连续时间Markov决策过程下的关系,在强互模拟关系的基础上,定义弱互模拟等价关系及强(弱)模拟关系,证明了这些关系之间内在的联系,同时研究了互模拟关系下的逻辑保持问题,阐述了强互模拟等价与asCSL(action and state base CSL)逻辑等价性的关系,证明了弱互模拟等价与CSL (Continuous Stochastic Logic)逻辑等价性的联系。(4)采用排队系统构建云计算平台的随机模型,阐述云计算系统能耗与调度概率之间的关联关系,以降低系统能耗为目标,提出基于遗传算法的调度概率优化算法。然后应用随机模型检测技术将计算节点的DPM (Dynamic Power Management)模型建模为连续时间Markov回报模型,并使用概率模型检测工具PRISM对节点能耗进行分析。(5)研究具有混合特征的混合Petri网和流体随机Petri网,分析其内在的建模机制。提出了一种一阶混合Petri网转换成流体随机Petri网的形式化方法,并指出转换得到的流体随机Petri网可以对部分变迁进行合并以减少模型的复杂度,给出变迁合并的算法,证明了转换和合并方法的正确性。阐述了流体随机Petri网模型下基于扩展CSL时态逻辑的模型检测方法。
[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.
【学位授予单位】：合肥工业大学
【学位级别】：博士
【学位授予年份】：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.
【学位授予单位】：合肥工业大学
【学位级别】：博士
【学位授予年份】：2016
【分类号】：O211.62;TP301.1
【相似文献】
相关期刊论文 前10条
1 陈清亮;朱可宜;;多智能体协同的认知规范模型检测算法[J];中山大学学报(自然科学版);2009年01期
2 周从华;邢支虎;刘志锋;王昌达;;马尔可夫决策过程的限界模型检测[J];计算机学报;2013年12期
3 吉猛;胡克瑾;;基于模型检测的电子商务鉴证技术[J];陕西师范大学学报(自然科学版);2006年04期
4 宁正元;胡山立;赖贤伟;;交互时态信念逻辑及其模型检测[J];南京大学学报(自然科学版);2008年02期
5 王曦;徐中伟;梅萌;;基于模型检测的软件安全性验证方法[J];武汉大学学报(理学版);2010年02期
6 王晶;张广泉;;基于概率时间自动机的模型检测反例表示研究[J];苏州大学学报(自然科学版);2011年02期
7 高妍妍;李曦;周学海;;L4进程间通信机制的模型检测方法[J];中国科学院研究生院学报;2011年06期
8 王扣武;张s，
本文编号：2125934
本文链接：https://www.wllwen.com/shoufeilunwen/xxkjbs/2125934.html
