形式化方法是使用数学方法确保计算机软硬件系统的正确性和可靠性.经典的形式化描述和验证方法是在二值逻辑上展开的.近年来,大家开始关注非二值情形的形式化描述和验证方法研究,逐步形成了量化描述和验证方法,包括数值和非数值的形式化描述和验证方法.本文将剩余格理论和形式化方法两个不同的研究领域联系起来,提出了一种描述不完备或不相容信息的系统和满足系统量化验证需要的形式化模型,显著地增强形式化模型的表达能力和应用能力,形成一种新的非数值(格值)量化验证理论.主要研究内容如下：(1)在论文的第三部分,为了对不完备或不相容信息的系统进行形式化描述和满足对系统进行量化验证的需要,根据经典的双标号转换系统,我们提出了基于完备剩余格的双标号转换系统作为此类系统的一般模型.格值标号转换系统和格值Kripke结构是格值双标号转换系统的两种特殊的情形.在格值双标号转换系统框架下,我们将传统的互模拟等价关系、模拟等价关系和模拟关系扩张到格值情形,来度量系统之间的接近程度,给出了寻找这些关系的算法.通过引入格值μ-演算的概念,分析了格值μ-演算的模型检测可判定性问题,给出了格值互模拟等价、格值模拟等价关系、格值模拟关系的逻辑刻画.最后,将格值互模拟等价和抽象解释的思想结合起来,讨论其与格值模型检测的关系.(2)在论文的第四部分,我们将传统的系统之间的迹包含和迹等价关系扩张到格值上我们讨论了在基于完备剩余格的Kripke结构上,如何将传统的迹包含和迹等价语义推广到完备剩余格环境下,提出了三类不同的格值迹包含和迹等价定义,分析它们的基本性质.通过对线性时态逻辑进行语法扩张,将语义解释在格值Kripke结构上,证明了格值线性时态逻辑可以逻辑刻画格值包含和迹等价关系.(3)在论文的第五部分,我们研究了格值标号转换系统和格值Kripke结构之间的相互关系.论文通过给出两种模型相互转换的方法,分别证明了模型的相互转换是保系统状态上的格值互模拟关系的.我们也分析了格值模态逻辑和格值HML逻辑之间通过引入翻译函数,借助于两种模型之间的相互转换方法,逻辑公式语义真值在转换过程中的一致性.我们也研究格值CTL逻辑的一些重要的问题,如不动点语义和路径语义的关系,模型检测问题的可判定性问题.也论证了解释在格值Kripke结构上的格值模态逻辑和解释在格值标号转换系统的格值HML(?)逻辑,在转换过程中,公式的真值是不变的.另外,我们也分析了格值计算树逻辑的一些基本性质.(4)在论文的第六部分,为了描述和分析不相容或不完备信息的实时系统,在时间自动机的基础上提出了基于完备剩余格的格值时间自动机模型,其操作语义建立在格值双标号转换系统的一个变体上,分析了它的可达性问题的可判定性.我们提出了一种格值实时时态逻辑,来描述格值时间自动机所描述的系统的特性,给出了它基于格值时间自动机的模型检测算法.最后,引入了一种新的互模拟概念来刻画格值时间自动机状态之间的关系,证明了我们的格值实时时态逻辑能逻辑刻画这种概念.