The Software Safety Verification Methodology Based On Fault-extended Statecharts

Software has been widely applied in safety critical area. The reliability of software becomesincreasingly important. In order to improve the software quality, the safety analysis methods ofsoftware model have always been hot topics in both academia and industry. The analysis methodsbased on traditional UML statecharts are able to decide whether the behavior of components satisfiesthe requirement. However, they cannot analyze the fault effectively, and can only depend on theexperience of experts to extract the safety attributes. Fault tree is able to fully describe the factors ofsoftware faults, but cannot decide whether they exist in software system.In this paper, we propose a new concept called fault-extended statecharts, combining UMLstatecharts and fault tree, for the analysis and verification of software safety. We integrate thefault-extended statechart with the model checking technique to perform the automatic verification.The main contributions of this paper are as follows:1. A new concept called fault-extended statecharts is proposed, combining UML statecharts andfault tree. It unifies the functional model and the safety-requirement model of software. The feasibilityof safety analysis using the fault-extended statechart is given.2. The construction method of fault-extended statechart is proposed. The statecharts of system isextended with the information extracted from the fault tree, using the gate conversion rules.3. A modeling and verification method based on fault-extended statechart is proposed toenhance the safety of software. In this method, we apply the model checking technique to verify thesafety properties of software, by analyzing the reachability of the fault states according to theproperties of fault-extended statechart.4. An illustration of a case study of microwave control system is given to explain the feasibilityand effectiveness of our method. The modeling and verification of fault-extended statechart isperformed under ESpin, a model checking environment we have developed.