形式化方法是指依赖严格的数学基础对软、硬件系统进行形式规约、开发和验证的技术。形式规约作为形式化方法的基础,通过形式语言严格描述所开发系统的模型和其需要满足的性质,包括模型规约和性质规约。而性质规约分为线性时间规约和分支时间规约,安全性和活性作为这两种性质规约中的基础属性,已经得到了广泛的研究。安全性断言系统运行时“坏”的事情不会发生,而活性断言系统运行时“好”的事情最终会发生。安全性和活性的验证为系统的可靠性提供保障。随着系统的日益庞大和复杂,不可避免地会出现不确定或者不一致信息的处理。在经典的形式规约中加入模糊理论是一种有效的量化方法,可以对模糊系统的行为进行精确地刻画。性质规约中的分支时间规约对于系统验证有着非常重要的作用,将分支时间属性扩展到模糊系统中还没有相应的形式化定义,同时安全性和活性的量化扩展将为模糊系统的验证提供理论基础。本文基于模糊Kripke和模糊迁移系统,研究安全性和活性推广问题及其推广之后的性质,主要工作如下:1、基于模糊Kripke结构,文中给出了性质规约中分支时间属性在模糊背景下的形式化定义,重点研究了其中的安全性和活性。同时定义了两种闭包操作,从而产生了四种类型的属性:泛安全性、泛活性、存在安全性和存在活性。最后,证明了每个分支时间属性,或是存在安全性和存在活性的交,或是泛安全性和泛活性的交,或是存在安全性和泛活性的交。这些将为模糊模型检测的进一步发展提供理论支撑。2、基于模糊迁移系统,对经典的安全性和活性进行了定量扩展,定义出α-安全性和α-活性,给出了α-安全性和α-活性的两种前缀和闭包操作,证明了如何判定一个属性是α-安全性和α-活性的判定定理,进一步给出了将一个属性分解为α-安全性和α-活性的分解结果。最后引入一个实例来阐述这些结论在实际应用中的适用性。