Research On Software Safety Analysis Methodology Based On State/Event Fault Tree

The embedded softwares are widely used in fields of astronomy, nuke industry, transportation, etc. And the safety of embedded softwares shows great significance for system safety. Nowadays, more and more attention has been paid to software safety in both academic and industry area. There are two main methods for software safety analysis: one is analyzing software safety requirements, while the other is software function design. However, the above two methods are usually independent in software development. Considering it, the analysis results of software requirements cannot be used in the phase of function design, it is hard to analyze the software safety requirements in the phase of software function design, and to carry out the analysis work of software safety based on software function design model. Existed safety analysis based on fault tree can neither describe the model behaviors, nor determine the causality of faults whether exists in function model design. The software design model based on statechart, able to describe model behaviors, but it is hard to reveal the hidden faults.Targeting the problems above, this thesis proposes an analysis method of software safety based on State/Event Fault Tree(State/Event Fault Tree, SEFT). This method uses SEFT to describe the fault causality and the interior model behaviors of fault triggering. Then we abstract the rules of safety requirement, and expand it to a statechart. Finally, we verify and analyze the expanded chart by model checking. This detailed discussion of this thesis is as follows:(1) Use SEFT to describe both software failures and the causality of inside model behaviors. The corespondent sequence chart, resulting in a Liner Temporal State/Event Fault Tree(Liner Temporal SEFT, LTSEFT), is realized using sequence timing logic. We use the reduction rules to reduce this tree, and abstract the LTL rule from it based on its smallest cut set.(2) Define the transformational rules for SEFT logical gate to statechart. Then we design safety requirement chart mapping safety requirements to statechart elements. Also, an automagical construction algorithm has been designed based on this mapping chart and transformational rules.(3) Transfer expanded statechart to Promela via model transformation, then put it into SPIN. The further verification and analysis of software safety will be conducted according to the LTL reduction of the information abstracted above.In sum, this thesis provides a method of case analysis for "flap and slat control system". Then we describe the progress of SEFT and LTSEFT construction, abstract the LTL rules. At the end of this thesis, we verify and analyze the transferred Promela to prove the effectiveness of our method. We believe that this method offers a brand new thinking for analysis of embedded software safety.