论文部分内容阅读
随着计算机软硬件系统日益复杂,如何保证其正确性和可靠性,已成为大家广泛探讨的问题.模型检测由于其借助严格的数学方法来验证系统是否满足性质和自动化验证等特点,深受学术界和工业界的关注.经典的模型检测是一种定性的验证方法,其强调的是系统满足功能需求性质的绝对正确.然而很多实际的系统被赋予量化行为特征,需要定量分析其满足用户的功能和非功能需求性质的程度.近年来,学者们开始研究定量的模型检测.定量的模型检测不仅能体现系统多大程度满足其功能需求性质,还能体现系统的性能指标等非功能需求,极大地拓展了模型检测的应用范围.定量的模型检测包括概率模型检测和模糊模型检测,其中概率模型检测用于验证概率系统,对具有不确定信息和不相容信息的非概率系统,学者们提出了模糊模型检测.广义可能性模型检测是模糊模型检测的主要形式之一,由于其考虑了测度信息,它能更完善地验证模糊系统的性质.本文主要针对模糊系统,引入广义可能性决策过程(generalized possibilistic decision process,GPDP)模型来描述此类模糊系统的行为.利用可能性测度理论和决策过程的相关理论,将经典的计算树逻辑(Computational Tree Logic,CTL)、线性时间属性、线性时态逻辑(Linear Temporal Logic,LTL)和分支时态逻辑CTL*等的模型检测方法以及互模拟等价验证方法拓展到广义可能性决策过程(GPDP)上.本文的主要结论包括以下三个方面:1.基于决策过程的广义可能性计算树逻辑模型检测:给出了用于描述模糊系统行为的广义可能性决策过程(GPDP)模型,引入了GPDP上的调度的概念,定义出广义可能性测度并给出了其计算方法.为了更好地描述模糊系统的性质,同时引入了广义可能性CTL(Generalized Possibilistic CTL,GPoCTL)的语法,且给出GPDP上的GPoCTL的语义.利用上述提出的广义可能性测度理论,分别给出了最大可能性调度和最小可能性调度对应的GPoCTL模型检测算法,该算法的优点在于将GPoCTL模型检测的验证过程转换为模糊矩阵的运算和不动点的计算.2.基于决策过程的广义可能性线性时间属性模型检测:为了描述广义可能性线性时间属性,引入了广义可能性LTL(Generalized Possibilistic LTL,GPoLTL)的语法,给出了GPDPG上的PoLTL的路径语义和语言语义,并证明了这两种语义是等价的.利用提出的广义可能性测度理论,重点讨论了最大可能性调度和最小可能性调度对应的最终可达性、总是可达性、持久可达性和重复可达性等可能性线性时间属性的模型检测方法,该方法的优点在于将它们的模型检测的验证过程转换成模糊矩阵的运算或不动点的计算.最后,研究了广义可能性正则安全属性和广义可能性纠-正则属性的模型检测问题,分别将它们的模型检测问题转换成广义可能性线性时间属性总是可达性和重复可达性的模型检测问题.3.基于决策过程的广义可能性CTL*模型检测和最大可能性互模拟:引入了广义可能性CTL*(Generalized Possibilistic CTL*,GPoCTL*)和GPoLTL的正规范型(GPoLTL Positive Normal Form,GPoLTLPNF)的语法,给出了GPDPG上的GPoCTL*语义和GPoLTL PNF语义.利用提出的广义可能性测度理论,重点研究了:(1)最大可能性调度和最小可能性调度对应的GPoLTL PNF模型检测算法,该算法将GPoLTL PNF模型检测的验证过程转换为模糊矩阵的运算和不动点的计算;(2)将GPoCTL*模型检测问题转换成GPoCTL模型检测问题或GPoLTL模型检测问题的方法.最后,针对模糊系统的等价性验证问题,引入了最大可能性互模拟的相关概念,研究了它的逻辑刻画。