模型检测是80年代初由Clarke和Emerson提出的,是一种有效的自动化验证技术,可用于检测计算机硬件和软件的正确性。由于模型检测可以自动执行,并能在系统不满足性质时输出反例路径,因此被广泛应用,并取得了令人瞩目的成果。但随着现实系统的复杂化,模型检测技术必须更新以解决两方面的问题,一是处理系统中所含的不确定信息,二是处理系统验证中的状态爆炸问题。模糊Petri网可直观简洁地描述复杂的并发系统,因此研究基于模糊Petri网的复杂系统模型检测具有一定的实践意义。本文从以下两方面展开研究,以解决复杂系统模型检测中的不确定信息处理问题和状态爆炸问题。1.给出基于模糊Petri网的LTL模型检测方法。首先将模糊Petri网转化为一种特殊的可达图:该可达图中的状态标识符是一个矢量,且矢量中的每个元素取值在[0,1]区间上;在状态间的迁移关系上也有一个[0,1]区间上的参数;然后将该可达图转化为广义可能性Kripke结构(GPKS);在此基础上,可以利用广义可能性模型检测算法完成验证,从而有效地解决了复杂系统模型检测中的不确定信息处理问题。2.给出分布式模型检测算法。首先依据状态关系对GPKS进行划分,使关系紧密的状态尽可能地划分在一个计算节点上,为分布式验证算法的执行效率提供良好的基础;定性性质使用Buchi自动机表示,定量性质使用模糊自动机表示,在不同的计算结点上,利用扩展的LTL分布式模型检测算法完成定性验证和定量验证,从而有效地缓解了复杂系统模型检测中的状态爆炸问题。本文的贡献在于:提出了广义可能性测度下的LTL分布式模型检测方法,可缓解广义可能性测度下的模型检测所面临的状态爆炸问题;为现实环境中的复杂系统的模型检测提供了一个可行的方案。