构件系统被广泛应用于许多工业领域,全面的分析其行为和正确性具有现实需求和意义。现已有对该系统交互及随机行为正确性进行验证的符号化、组合和统计模型检测方法。由于构件系统中变量较多,容易引起验证的状态空间爆炸问题;而使用抽象技术时,验证是不完备的。针对以上问题,围绕对构件系统中变量的处理,本文提出了一些模型检测方法,并将它们用于实际案例的的验证。本文的主要贡献如下:?本文提出了基于变量划分的符号化模型检测方法。该方法对分离迁移表达式中的变量集合进行划分,将其分为值变化和值不变的两个子集。使用该方法进行构件系统符号化模型检测时,只需要对迁移上值变化的变量进行处理,有效地减少了时间和内存开销。?本文针对组合抽象构件系统不变式验证的不完备问题,提出了不变式增强和状态划分两种精化方法。不变式增强方法主要用于去除系统伪反例,并生成增强不变式精化原系统不变式;状态划分方法主要利用反例对抽象状态进行划分,生成新状态对抽象系统进行精化。将上述两种精化方法融入到组合抽象方法中,本文提出了构件系统抽象精化组合模型检测算法,并证明了该算法的完备性和有效性。?为了对随机构件模型行为属性进行概率分析和检测,本文设计并实现了模型翻译和基于模块的系统组合方法,其保留了原模型的概率信息和构件系统的组合特性。本文使用概率变量分布离散化方法对复杂模型进行抽象,并对抽象模型的概率模型检测和原模型的统计模型检测方法进行比较和分析。?为了分析带权随机构件系统期望的性质,针对已有i LTL方法只能对非周期Markov模型进行验证的问题,本文提出了对周期Markov模型的概率质量函数(pmf)序列的时序属性进行基于可行解的模型检测方法——ip LTL。上述验证方法使用了抽象技术,将pmf作为模型状态。当待验证属性不成立时,该方法将给出反例,即模型的初始pmf。从该初始pmf出发,可以对违反属性的系统运行进行分析。