摘要
民航业务系统正确处理民航业务逻辑是民航企业运行的必要条件,因此民航业务系统的安全性十分重要,形式化验证方法是保障系统安全性的重要技术手段。本文结合故障树分析技术提取民航业务逻辑的安全性验证需求,并用新提出的ABPD业务流程模型为民航业务系统建模,进一步分析并定义出6种安全性性质。最后,采用图搜索方法对ABPD模型进行安全性验证并给出具体算法实现。实验结果表明了算法和程序的有效性。
The safety of the civil aviation business system is very important because it is a necessary condition for civil aviation enterprise to run.Formal verification method is an important approach to insuring system safety.In this paper, firstly, the fault tree analysis technology is introduced to analyze the safety requirements and the new ABPD modeling language is promoted.Sec-ondly, six kinds of safety properties are defined through analyzing the model.Thirdly, safety verification is achieved through graph search algorithm and the concrete implementation of the algorithm is provided.Lastly, the experiment results explain the completed verification process and the validity of the method.
出处
《计算机与现代化》
2014年第10期46-51,65,共7页
Computer and Modernization
基金
国家重点基础研究发展计划项目(2014CB744900)
关键词
民航业务系统
故障树分析技术
ABPD模型
安全性验证
模型验证
civil aviation business system
fault tree analysis technology
ABPD modeling
safety verification
model verification
