模型检测作为一种形式化的自动验证技术,可在设计和开发过程对系统的功能和性能进行分析与验证,从而保证系统在运行过程中的正确性及可靠性。然而由于系统的复杂性及验证属性的多样性,模型检测的相关理论与技术还有待发展与完善。本文主要针对随机模型检测中的时空性能分析所涉及的一些重要内容进行研究,主要包括以下几个方面：(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时态逻辑的模型检测方法。