随着信息技术的快速发展,各种软、硬件系统在社会生活中占据着越来越重要的位置,系统的安全性与可靠性因此变得越来越重要。功能正确性与性能可满足性日益成为学术界关注的热点问题,采用有效的手段来验证系统的功能及性能特征是否满足要求已成为日益重要的研究课题。形式化方法被认为是系统性能可信评估方面可行、有效的方法之一。其中模型检测技术因其自动化程度高且具有严格的数学基础等优点而被广泛应用,研究热点包括硬件验证、协议分析等领域并逐渐转移到软件验证领域,关注的重点也由对系统行为的定性分析转向定性分析与定量分析相结合的复杂参数性质验证。对于包含多种参数特征的复杂随机系统,模型检测的首要问题就是如何对系统进行精确地建模并进行性质特征的有效刻画,此外传统模型检测技术中出现的状态空间爆炸问题以及如何采用高效的复杂随机系统性质验证算法并对反例信息进行有效表示与理解,亦成为影响复杂随机系统模型检测技术应用、普及的新障碍。因此,对模型检测理论及其在复杂随机系统领域的应用进行深入研究具有较高的理论和应用价值。针对模型检测在复杂随机系统验证中面临的主要问题,本文开展了以下几个方面的工作。(1)对模型检测技术中的时序逻辑及模型表示方法进行综合分析,提出了一种用于复杂随机系统性质描述的新型连续随机逻辑aCSRL,并给出对应的系统模型建模表示方法,相应的模型命名为CTMRDP,对模型的动态行为做出严格的表达的同时,对比分析了 aCSRL与现有的用于复杂随机系统性质描述的相关时序逻辑,证明了其表达能力严格强于相关的其它连续逻辑。(2)提出了用于复杂随机系统模型CTMRDP的aCSRL性质验证方法。通过特征消去、强连通子图构造等步骤,采用类似CSL模型检测的方法完成了 aCSRL稳态概率状态公式的求解并进行实例分析。对于aCSRL瞬时概率状态公式,通过对其所包含的路径公式的结构分析,基于自动机理论给出了 aCSRL路径公式的形式化表示,借鉴传统的LTL模型检测方法,给出了路径公式自动机与系统模型的同步自动机模型的定义,提出了基于同步自动机模型下的时间、回报特征约束下的性质定量验证方法,并进行了算法描述,通过实例分析证明了复杂随机系统模型aCSRL时序逻辑性质验证的可行性与有效性。(3)针对离散概率回报模型,提出了多重直到约束路径公式及条件概率状态公式的逻辑语义,通过构造多重直到公式及多重直到合取公式自动机,基于同步自动机模型对相应的性质验证方法并进行了实例分析,同时基于离散概率回报模型转化得到的带权有向图,采用迭代求解方式提出了多重直到约束路径公式及条件概率状态公式定量验证求解算法,通过实例构造分析证明了算法的有效性,同时提出了离散概率回报模型性质反例的正则表达式压缩表示方法以及反例自动机模型表示方法。(4)针对复杂随机系统模型性质验证的状态空间爆炸问题,提出一种应用于马尔可夫回报模型的状态空间约减的方法。该方法首先利用符号编码方式对模型进行二元决策图表示,而后利用对称约减技术,结合了互模拟理论通过分析原始模型中的等价类关系,借助等价类唯一表示函数,基于状态迁移矩阵给出了模型约减算法,通过实例分析证明了方法的有效性,适当改进后可方便地推广到其它的复杂随机系统模型,有效缓解模型检测过程中的状态空间爆炸问题。