软件系统的正确性一直是人们所关心的问题,人们使用各种方法来验证一个软件系统的正确性,目前已经有越来越多的人使用模型检测技术来对软件系统进行验证,也就是通常我们所说的形式化方法验证。本文我们将使用FeaVer对Kerberos系统中的源代码进行形式化验证,并找到了其中的错误代码。验证时使用测试用具对验证模型进行提取,再使用集成的验证工具对其进行验证便可检测出系统违反的正确性属性,我们证明了Kerberos系统中绝大部分的源代码都是正确的,但同时我们也证明了在其源代码中也确实存在错误,并找到了出错的代码。于是我们在验证结果的基础上对原来的验证模型进行了修改,并且建立了新的模型。经验证新模型符合我们所定义的正确性属性。最后我们以新模型为依据对Kerberos的源代码进行了改进,使系统达到了一个更可靠的状态。