民航业务系统的安全性分析与验证

民航业务系统正确处理民航业务逻辑是民航企业运行的必要条件,因此民航业务系统的安全性十分重要,形式化验证方法是保障系统安全性的重要技术手段。本文结合故障树分析技术提取民航业务逻辑的安全性验证需求,并用新提出的ABPD业务流程模型为民航业务系统建模,进一步分析并定义出6种安全性性质。最后,采用图搜索方法对ABPD模型进行安全性验证并给出具体算法实现。实验结果表明了算法和程序的有效性。