| As an important filed of social development and national economy, civil aviation processes thecharacteristics of high investment, high technology and high risks. Development of airline business isaffected and restricted by the safety level of civil aviation business system. With the development ofcivil aviation business, the civil aviation systems enhance rapidly, and the scale becomes huger andmore complex. It is imperative to verify the safety of business system model in the design phrase.Aiming at this requirement, the safety of civil aviation business systems are analyzed and verified inthis paper. The main research contents are as follows:(1)The fault tree analysis technology is introduced to analyze the safety of civil aviation businesssystem model. The typical accidents are analyzed and summarized for dispatch business system basedon the fault tree to find out the cause of the unsafe events and qualitative analysis technology isadopted to acquire the safety requirements.(2)A novel civil aviation business system model-ABPD is established. The dependentrelationships between the data is introduced into the traditional business process model, then ABPDmodel based on directed graph containing both business process model and data model is put forward.ABPD can express the logical relationship between the tasks in the sequence flow, and can describethe data logical relationship as well.(3)Safety properties are established and verification method is put forward. According to therequirements of civil aviation safety aiming at restricting the unsafe events,6kinds of securityproperties are defined. According to the properties of safety and ABPD model, a novel verificationmethod is presented to verify the safety based on traversal method.(4) Implementation of safety verification. First XML is introduced to describe the ABPD model,the relationships between the nodes in the model are analyzed to show the model data structures. Then,the system modules are analyzed and the verification algorithm is discussed further. At last averification tool prototype is programmed based on MFC to show the effectiveness of the algorithm. |