形式化验证是以数学理论为基础,来确保计算机软硬件系统的正确性和可靠性.经典的形式化验证是基于二值逻辑展开的,它并不能用于处理含有量化信息的系统验证问题.因此,量化形式化验证应运而生,为含有量化信息的系统验证提供了一种有效的验证方法,受到了学术界和工业界的重视.模糊系统的形式化验证是量化形式化验证中的一个重要研究方向.当前关于模糊系统的形式化验证方法的研究还处于起步阶段,自动化的模型检测技术和系统合成技术尚未得到深入研究.其主要原因是模糊逻辑的多样性和模糊系统的复杂性使得很难给出有效的形式化验证方法.本文的目的是解决模糊系统的验证问题,主要包括模糊系统的模型检测问题和模糊线性时序逻辑的系统合成问题,以及模糊开放系统的可达性验证问题.主要贡献如下:(1)提出了基于模糊系统的计算树逻辑的模型检测方法.引入了不确定型模糊Kripke结构作为模糊系统的模型.给出了模糊计算树逻辑的语法和语义,用于刻画该模型的分支时序性质.提出了基于不确定型模糊Kripke结构的模糊计算树逻辑的模型检测算法,使得该模型检测过程可以在对数多项式时间内完成.(2)研究了基于不确定型模糊Kripke结构的模糊计算树逻辑在公平语义下的模型检测问题.为确保模型检测是在不确定型模糊Kripke结构中的公平路径上进行验证,引入了基于不确定型模糊Kripke结构的模糊计算树逻辑的公平语义.给出了模糊计算树逻辑在公平语义上的模型检测方法.(3)为了解决模糊线性时序逻辑的可实现性验证问题,引入了模糊博弈,给出了在模糊博弈中任一参与人的获胜策略的构造方法.把模糊线性时序逻辑的系统合成问题归约为在模糊博弈中最优获胜策略的构造问题,分析了该归约方法的时间复杂性.(4)解决了模糊开放系统的可达性验证问题.引入了格值可达博弈图,作为模糊开放式系统模型.给出了两个参与人在格值可达博弈中的任意状态上获胜真值的计算方法,证明了两个参与人在任意状态上具有相同的获胜机会.把模糊开放系统的可达性验证问题转换为在格值可达博弈图中获胜真值的计算问题。