● 摘要
安全性是安全关键软件系统关键属性，软件系统的安全性问题多数来源于需求阶段，所以正确的需求对于确保安全性是至关重要的。为了确保软件系统安全，在软件系统投入使用之前必须进行安全性验证，目前，传统的需求验证技术即分析、评审、测试已不能满足安全关键软件对安全性需求的严苛验证要求，并且传统的软件安全性测试、分析越来越不能满足安全关键软件对安全性的要求，那么就需要一种有效的方法，能对软件错误进行正确、高效的检测和定位。而模型检测技术具有高度自动化和检测效率高的优点，模型检测的使用可以突破人脑的主观限制、消除主观差异，是实现软件需求安全性严格验证工作和提高验证效率的有力途径。
将模型检测技术应用于安全关键软件需求的验证方面，对安全关键软件进行需求形式化建模和模型检测可以提高其可信性，但是目前对其进行模型描述、属性提取方面还存在局限性,尤其是往往采用人工定义的办法去进行属性的形式化描述。本文提出一种结合FTA（Fault tree analysis）和模型检测的形式化验证方法来验证目标系统的安全性，系统模型用基于FSM（Finite State Machine）的方法来描述，用基于FTA与模型检测相结合的方法获取待验证系统的安全属性，最后给出在飞行控制软件系统的应用，构建了系统FSM模型及安全属性模型，然后利用模型检测工具NuSMV对模型进行检验，并给出反例路径以进行错误分析。过程和结果表明该方法可以有效的支持实际的软件安全性需求的建模和验证。