In order to ensure the safety of railway station interlocking system, the subsystem for route creating is used as a case study, and a formal modeling method based on multiple composite scenarios analysis is provided. In the proposed method, multiple UML sequence diagrams are adopted to specify requirements of the system, and consistent requirements specification are acquired by combining pre-condition and post-condition of object constraint language with domain knowledge to analyze conflicts in multiple UML sequence diagrams. Besides, a model conversion method for transforming behaviour sequences to finite state process model is proposed, despite these behaviour sequences are usually synchronous, asynchronous, concurrency and alternate, which interacted with each other in UML sequence diagram. Finally, an FSP model for system's formal model is generated by combinatorial operation, it is conformed to system's functional requirements. The correctness and feasibility of the proposed method have been confirmed by formal model generation for railway station interlocking system.
展开▼
