Safety Analysis and Verification on Civil Aviation Business System

doi:10.3969/j.issn.1006-2475.2014.10.011

Abstract

Abstract: 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. Secondly, 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.


Key words: civil aviation business system, fault tree analysis technology, ABPD modeling, safety verification, model verification

CLC Number:

TP302.1

XING Ni-zhou, WANG Li-song. Safety Analysis and Verification on Civil Aviation Business System[J]. Computer and Modernization, doi: 10.3969/j.issn.1006-2475.2014.10.011.

References

［1］王文哲. 浅谈中国民航信息化重要性［J］. 企业导报, 2011(14):199.
［2］李小燕,肖雄飞. 中国民航发展中的安全问题［J］. 中国民用航空, 2004,4(12):8-48.
［3］廖军,谭浩,刘锦德. 基于Pi-演算的Web服务组合的描述和验证［J］. 计算机学报, 2005,28(4):635-643.
［4］付茂洺,王悠. 可视化UML模型验证环境研究［J］. 电子科技大学学报, 2010,39(2):289-293.
［5］ Van Der Aalst W M P. Workflow verification: Finding control-flow errors using petri-net-based techniques［M］//Business Process Management. Springer Berlin Heidelberg, 2000:161-183.
［6］ Touré F, Bana K, Benali K. An efficient algorithm for workflow graph structural verification［M］// On the Move to Meaningful Internet Systems: OTM 2008. Springer Berlin Heidelberg, 2008:392-408.
［7］ Sadiq W, Orlowska M E. Applying graph reduction techniques for identifying structural conflicts in process models［C］// Proceedings of the 11th Conference on Advanced Information Systems Engineering. 1999:195-209.
［8］ Sadiq S, Orlowska M E, Sadiq W, et al. Data flow and validation in workflow modeling［C］// Proceedings of the 15th Australasian Database Conference. 2004,27:207-214.
［9］ Sadiq W, Orlowska M E. Analyzing process models using graph reduction techniques［J］. Information Systems, 2000,25(2):117-134.
［10］OMG. BPMN2.0 (Standards style), BPMN Standard［S］.
［11］Thomas Allweyer. BPMN 2.0-Business Process Model and Notation［M］. Books on Demand GmH, 2010.
［12］Trka N, van der Aalst W M P, Sidorova N. Data-flow anti-patterns: Discovering data-flow errors in workflows［C］// Proceedings of the 21st International Conference on Advanced Information Systems Engineering. 2009:425-439.
［13］Russell N, ter Hofstede A H M, Edmond D, et al. Workflow data patterns: Identification, representation and tool support［C］// Proceedings of 24th International Conference on Conceptual Modeling. 2005:353-368.
［14］van Der Aalst W M P, ter Hofstede A H M, Kiepuszewski B, et al. Workflow patterns［J］. Distributed and parallel databases, 2003,14(1):5-51.
［15］杨红丽,刘建元,韩俊刚. 基于PVS的飞机订票系统的形式化描述与验证［J］. 西安邮电学院学报, 2001,6(3):1-4.
［16］Yang Y, Keller P, Livnat Y, et al. Improving safety-critical systems by visual analysis［C］// VLUDS. 2011,27:43-58.
［17］Conforti R, Fortino G, La Rosa M, et al. History-aware, Real-time Risk Detection in Business Processes［M］// On the Move to Meaningful Internet Systems: OTM 2011. Springer Berlin Heidelberg, 2011:100-118.

[1]	OU Jin-rong, XU Jun-shan. Application of Mobile Payment in Subway Ticket Vending Machine System [J]. Computer and Modernization, 2018, 0(10): 106-.
[2]	ZHANG Zhong, ZHU Tian-tian, MA Xing-lu. Design of Child Anti-lost System Based on NB-IoT [J]. Computer and Modernization, 2018, 0(02): 30-.
[3]	ZHANG Xiao, WANG Li-song, RANG Tao. Preliminary Design of Model-based Integrated Modular Avionics Platform [J]. Computer and Modernization, 2016, 0(6): 29-35,39.
[4]	XING Ni-zhou, WANG Li-song. Safety Analysis for Avionics System Based on Model Driven [J]. Computer and Modernization, 2015, 0(1): 21-26.
[5]	HOU Li-min, ZHANG Yong-qiang. Course-oriented Chinese FAQ Auto Question Answering System Model [J]. Computer and Modernization, 2014, 0(10): 20-24.
[6]	XU Lei1,2, ZHOU Xi1, MA Yupeng1, WANG Lei1. Design and Implementation of RFID Middleware Based on NFC Mobile Devices [J]. Computer and Modernization, 2014, 0(9): 90-94.
[7]	XIA Ye-feng;XU Jun-shan. Application of Multi-threading Technology in Subway Ticket Vending Machine Software [J]. Computer and Modernization, 2013, 218(10): 193-196,.
[8]	LIU Xiao-xi;LI Zhuo-yue. Load Balancing of Cloud Environment Based on Optimized Ant Colony Algorithm [J]. Computer and Modernization, 2013, 1(9): 42-45.
[9]	ZHOU Ya-guang;HU Xiao-ji. Design and Simulation of CPCI-E Backplane [J]. Computer and Modernization, 2012, 1(11): 203-208.
[10]	WANG Rui-juan. Research on SOA Used in Information System of Party Affairs Management [J]. Computer and Modernization, 2011, 193(9): 207-209.
[11]	GUO Ling. Design of Manufacturing Enterprise IT Services Platform [J]. Computer and Modernization, 2011, 1(3): 66-69.
[12]	HU Yao-min;. Research and Implementation of Ambiguous Path Indentification Based on RFID Dual Frequency Card [J]. Computer and Modernization, 2010, 1(11): 180-183.
[13]	REN Bing-zhong;KONG Wen-huan . Design and Implementation of GPS Vehicle Navigation and Guide System  [J]. Computer and Modernization, 2010, 1(01): 40-43.
[14]	LIU Yu-xian;MAO Xin-peng. Design and Implementation of Management Information System for Child Plan Immunity Based on C/S and B/S Modes [J]. Computer and Modernization, 2009, 8(8): 76-79.