Abstract: An important operation for constructing reliable and safety software systems is system's safety analysis and verification by formal methods. Formal modeling for system is vital, which can affect the results of safety analysis and verification. We provided a method for generating formal system model based on scenarios analysis. The method adopted UMI_ sequence diagrams to specify system's requirement firstly. In order to get consistent scenario-based requirements, we combined pre-condition and post condition of object constraint language with domain knowledge to analyze conflicts in I1MI_ sequence diagrams. 13csidcs, we proposed a model conversion algorithm for transforming interactions of objc(is in UML sequence diagram to finite stated process. Finally,we generated a finite states model for system's formal mod- e1, which is conformed to system's functional requirements. The correctness and feasibility of the proposed method were confirmed by generating formal model for railway station interlocking system. The new method provides a good way for system's formal modeling,and improves safety duality in demanding for safety software's designing and development.

Key words: Safety-critical system,Safety analysis,Formal methods,Formal verification