缺陷和漏洞广泛存在于各种软件中,难以避免,由其引发的故障很容易给生命财产带来损害,甚至灾难性后果。应对这一问题的有效途径是设计有效合理的自动化的测试方法对软件系统可信度进行充分全面的验证。本论文对软件可信安全性验证研究从静态验证和动态检测两个角度分别着手。首先从静态检测角度,针对安全苛刻性编程标准,提出基于规则匹配的代码静态检测方法。构建易于表述及存储源码信息的源码表示模型,解决C++语言的灵活性和复杂性导致的难以对代码直接进行规则匹配的问题；设计解析树模型和存储转换模型,完成从源代码提取与规则有关的信息翻译为中间表示文件的源码解析过程；设计包含编程安全标准中全部有效规则的规则库模型用于对中间表示文件进行规则匹配和缺陷反馈；通过系统实现和实验验证方法的有效性。然后从动态检测角度,提出一种基于非确定性FSM模型的测试生成和测试验证方法。针对复杂软件系统状态行为转换不确定的问题,提出层次化建模方法,对不确定的状态转移进行聚类和分层建模,将其转化为分层子状态机间确定唯一的状态转移,解决软件设计规格不确定行为难以描述和生成测试用例的问题；提出从正则式模型产生测试集的方法,根据状态机与正则表达式的等价关系,构建状态机模型对应的的正则式模型,给出迁移覆盖算法从正则式模型生成测试集,解决软件系统控制流程中循环部分在用例中难以精确描述的问题；在正则式模型中加入不同触发参数作为用例特征,划分出不同特征的测试集,提高用例的验证能力和测试充分性。静态手段可以在软件开发早期发现程序中的潜在缺陷,及时止损,减少开发中后期的故障率,以较少的成本提高软件可靠性；作为静态手段的补充,动态检测从系统级全局角度发现软件系统的符合性错误、运行时故障、以及静态验证阶段未发现的缺陷,在开发中后期为其可信度和健壮性验证提供进一步有力支持。