随着计算机技术的不断发展,计算机软硬件系统已经深入渗透到实际生活中的各个领域,若这些系统一旦出错,将给人类带来不可承受的损失,所以,安全问题已经逐渐成为人们的重点关注对象,但随着功能逐渐强大、设计日益复杂的发展,如何降低这些目标系统的测试成本也逐渐成为人们有待解决的难题,目前为止,人们已经研究出了很多种安全测试方法,比如形式化安全测试、基于模型的安全测试方法、基于故障注入的安全测试、威胁模型和攻击树理论、基于风险的安全测试、模糊测试(Fuzz Testing)、基于属性的安全测试和基于白盒的安全测试方法等,在各种安全测试方法中,形式化的模型检测算法被证明是一种有效的可靠性和正确性的安全测试方法,不仅能够有效降低目标系统安全测试成本,而且能有效定位系统安全威胁,而有限状态机模型可以很好的为为各种软硬件系统建立状态迁移系统,被广泛应用到实际应用中,具有深厚的理论基础,本文利用有限状态机理论,首先通过研究目标系统建立状态机模型,随后在此基础上用形式化公式表示其安全属性模型,然后通过判断系统模型是否符合安全属性来验证分析目标系统的安全性。主要的研究工作包括：首先,通过对有限状态机理论的研究，来为目标系统建立状态迁移系统模型,介绍了几种如何解决状态爆炸的算法原理,并提出一种基于模型分解的解决状态爆炸问题的方法,为状态爆炸问题的研究提供一种理论参考；然后,研究故障树模型分析法理论和其时序逻辑形式化方法,在故障树模型的基础上加入时序逻辑,方便利用故障树理论来生成时序逻辑公式,此方法有助于形式化的描述模型的安全属性；最后,通过研究各种安全测试方法和测试工具的特点,选择合适的工具来进行形式化的安全测试,通过AB协议的仿真实验过程来证明本文提出的安全测试方法的有效性。本文的创新点在于给出了一种解决状态机模型状态爆炸问题的理论基础与算法过程，并利用故障树的时序逻辑化来建立安全属性规范,用CTL公式来描述安全属性规范,通过将有限状态机模型和故障树模型的结合,给出了一种有效的安全测试方法,并用实验证明此方法是高校的。