● 摘要
近年来，随着计算机科学技术和航空航天技术的飞速发展，计算机软件在航空航天系统中所占的功能比重越来越高。软件的规模以及复杂度的增大，使得软件的安全性问题也日益突出，虽然已经存在了一些传统的分析方法如故障树分析，并在工程中得到了一定的应用，但是这些传统的分析方法大都是主观的，高度依赖分析人员的经验，很难保证分析的完整性、一致性以及正确性。而近年来兴起的基于模型的软件安全性分析方法，是指系统设计和安全性分析工程师可以通过采用一个基于模型的系统研发过程来共享相同的系统模型，通过加入故障模式以及相关的可控物理系统，自动化的实现安全性分析，提高分析质量。在基于模型的安全性分析方法中，形式化的方法通过形式化语言描述系统，利用数学逻辑关系发现其他方法不易发现的不一致，不明确或者不完整，从而提高系统的可靠性及安全性。
在众多的形式化方法中，由Abrial J-R提出的Event-B方法是最新的方法之一，它是一种以数学为基础的方法，可以清晰、抽象、简明、精确的描述和验证软件系统及其性质，并且已经拥有了自动化工具平台Rodin的支撑，为模型检验，可执行代码生成等提供了强大的工具支持。本文就是基于Event-B自身的形式化分析方法，并结合一些安全性准则，将其转换为Event-B的形式化语言，实现分析的自动化，主要的研究内容如下：
1）利用Event-B进行安全性分析的过程框架研究。包括结合传统的开发过程利用Event-B进行安全性分析的过程框架以及基于Event-B的开发过程进行安全性分析的过程框架两种情况，将安全性分析过程软件的开发过程相结合，为方法的具体实施提供指导。
2）基于Event-B的软件安全性分析方法的研究。包括利用Event-B进行安全性分析的方法，如定理证明、模型检验和动态演示等，并在此基础上研究如何利用Event-B对安全性准则进行检验的方法，包括对通用的软件安全性准则的归类和形式化描述，利用Event-B语言对安全性准则进行描述和验证的过程，借助定理证明、模型检验和动态演示等方法在RODIN平台上实现准则验证的自动化。
3）实例应用。选取适当的安全性准则，对刹车软件系统进行安全性分析，应用本文提出的基于Event-B的准则描述和安全性验证的方法，以检验方法的适用性与可行性。