计算机与现代化
計算機與現代化
계산궤여현대화
COMPUTER AND MODERNIZATION
2014年
10期
46-51,65
,共7页
民航业务系统%故障树分析技术%ABPD模型%安全性验证%模型验证
民航業務繫統%故障樹分析技術%ABPD模型%安全性驗證%模型驗證
민항업무계통%고장수분석기술%ABPD모형%안전성험증%모형험증
civil aviation business system%fault tree analysis technology%ABPD modeling%safety verification%model verification
民航业务系统正确处理民航业务逻辑是民航企业运行的必要条件，因此民航业务系统的安全性十分重要，形式化验证方法是保障系统安全性的重要技术手段。本文结合故障树分析技术提取民航业务逻辑的安全性验证需求，并用新提出的ABPD业务流程模型为民航业务系统建模，进一步分析并定义出6种安全性性质。最后，采用图搜索方法对ABPD模型进行安全性验证并给出具体算法实现。实验结果表明了算法和程序的有效性。
民航業務繫統正確處理民航業務邏輯是民航企業運行的必要條件，因此民航業務繫統的安全性十分重要，形式化驗證方法是保障繫統安全性的重要技術手段。本文結閤故障樹分析技術提取民航業務邏輯的安全性驗證需求，併用新提齣的ABPD業務流程模型為民航業務繫統建模，進一步分析併定義齣6種安全性性質。最後，採用圖搜索方法對ABPD模型進行安全性驗證併給齣具體算法實現。實驗結果錶明瞭算法和程序的有效性。
민항업무계통정학처리민항업무라집시민항기업운행적필요조건，인차민항업무계통적안전성십분중요，형식화험증방법시보장계통안전성적중요기술수단。본문결합고장수분석기술제취민항업무라집적안전성험증수구，병용신제출적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.
