进入21世纪，软件在社会的生产生活中的作用日趋重要，从最基础的衣食住行，到各种关键的位置，都有不同的软件协助人类进行自动化操控，然而由于日益增长的复杂性，各种软件缺陷日益增多，软件开始呈现出难以信任的特征，用户开始越来越看重软件的可信程度，急需提供相应的关键技术对软件进行可信性度量。软件的可信性度量就是度量软件的可信程度，即“软件行为按预期方式实现预期目的的程度”。模型检验是形式化的自动验证方法，它首先将待验证系统建模为状态系统，然后将要验证的性质转换为相应的时态逻辑，使用模型检验工具自动遍历系统模型，检验系统是否满足相应的性质。相比较普通的人工验证方法，模型检验的速度快，准确率高，可以很好的实现自动化操作。本文在总结和分析了已有软件可信性度量方法的基础上，做了如下几方面工作：一是根据软件开发过程前期阶段的UML活动图，提出一种软件可信性模型检验方法。该方法用SPIN模型检验工具针对软件的UML活动图可信性进行模型检验。首先将UML活动图转换为模型检验工具SPIN所采用的PROMELA描述语言，将需要检验的可信属性转换为LTL时序逻辑，使用SPIN工具实现软件前期阶段的可信性分析；二是根据软件开发过程后期阶段的源代码，提出一种软件可信性模型检验方法。该方法用下推自动机PDA描述软件运行中的行为，用有限状态机描述FSA描述软件的非可信行为属性，输入模型检验工具MOPS以检验软件源代码中是否存在非可信行为，实现代码开发阶段的可信性分析；三是针对现有的软件可信性分析方法存在的问题，提出了一种面向软件生命周期的软件可信性分析模型。通过形式化方法与非形式化方法相结合，对软件开发生命周期中的各个阶段进行可信性分析，实现软件的可信评估，以全面、准确的反映软件的可信程度。