缺乏系统的科学的测试体系是一直以来影响安全软件测试可信度的根本问题。在现有的工程实践中,测试是实验性行为的认知和实施方案普遍存在,威胁着系统的安全性并且这一问题随着安全软件需求量的激增,职责范围的外延,规模的扩大和复杂度的提高变得越来越严重。因此,构造高效可信的安全测试方法和工具已经成为安全软件行业不可回避的挑战。本文以构建安全软件的安全性测试理论框架及其应用为主要研究目标,针对安全软件苛求质量的实际需求,以形式化测试为基础,根据安全软件的典型特征,从设计符合其特点的建模语言开始,构建了统一安全性验证和安全性测试的理论框架。该理论框架立足于研发安全软件的全流程而非纯粹测试的立场,在保证测试方法本身正确性的同时,设计了通过测试也可以证明软件实现是安全的理论框架和相应的测试序列生成方法,主要贡献体现在:1.定义了多形态时钟时间模型,设计了多形态时钟输入输出迁移系统,给出了相应语法和语义的形式化定义,提出了将时间模型从系统行为模型中分离出来的安全软件建模方法;2.提出了统一的安全性验证与测试序列生成理论框架。该理论框架站在安全软件全流程而非单一测试的角度,将对规约设计的安全性验证与软件实现的安全性测试融合在同一个理论框架中,证明了如果某个实现通过了基于满足安全性属性模型所生成的测试序列集合,那么该实现也满足期望的安全性属性的结论,并给出了相应的测试序列生成方法;3.构建了多形态时钟输入输出迁移系统的安全性测试方法,定义了多形态时钟输入输出一致性关系,设计了相应的符号测试方法。并在此基础上,为了满足安全软件防护能力测试的需求,进一步提出了采用规约变异的测试方法计算安全软件的故障测试序列集合,定义了基于安全故障模型的变异算子,给出了基于弱变异思想的诱导规则,设计了k周期诱导算法。为了展示方法的可行性,本文以某实际车载列车自动防护软件系统为例说明了基于多形态时钟输入输出迁移系统的安全测试理论在安全软件系统中的具体应用。