Research On Modeling And Analysis Techniques For Software Temporal Fault Tree

FTA (fault tree analysis) is a simple and effective way for the analysis of system reliability and safety. It was originally presented by the United States Bell Labs in reliability study on automatic control system of telephone dialing machine, which has been 50 years history and has played a huge role in safety critical areas. In the 1980, software reliability and safety became the scientific issue of particular concern. To meet the needs of software safety analysis, fault tree analysis method traditionally used for the analysis of hardware reliability and safety was migrated to software field, and has been further expanded. With the application of software in various systems, the descriptions of system failures are getting more sophisticated. It is difficult to use the existing fault tree for the descriptions, so people have to bring in some new logic gates, producing dynamic fault tree and temporal fault tree.The existing formal logic for the semantics of the temporal fault tree is concise and easy to understand, but poor in expression and without the support of the existing tools. At the same time, model checking is welcomed for its maturity and a high automation, but the extraction of property is difficult. How to find a logical language which is suitable for the descriptions of temporal fault tree's semantic and has existing tools'support is a focus on the combination of the two methods. Constructing and analyzing of fault tree is quite cumbersome, time consuming and very prone to error. How to construct and analyze the fault tree conveniently and test its correctness effectively is a challenge need to be addressed in the application of fault tree.For the above problems and needs, we expand the existing temporal fault tree based on TCTL, so that it can express more complicated faults and system specifications. We formalize the temporal fault tree semantics with TCTL and extract formal properties of top-level events in the form of TCTL which is easy to be validated by UPPAAL. According to the characteristics of software systems, we present a new approach of testing fault tree's correctness based on software testing technology. The method can effectively detect the faults made during the fault tree construction. At the same time, based on the Eclipse Graphical Editing Framework GEF and Rich Client Platform RCP, using JAVA, we design and implement a software for temporal fault tree analysis. The software has the functions for aided generation and automatic analysis of TFT, and can extract formal properties of the target events.