关键词: 项重写系统, 联锁, Maude语言, 安全苛求系统, 模型检测

Abstract: Modeling and verification methods require a rigorous methodology and technology for the integrity of the safety-
critical system modeling, which have incomparable advantages on the correctness, compared with the traditional methods. This paper proposes a method of using the Term Rewriting System to build the model, and using Maude based on Term Rewriting System to ensure the formal description and verification of interlocking system. With the syntax and semantics of Maude, the specification of various types of constraints and discrete events constitutes the properties and behavior of the interlock system. The safety properties and static properties of interlocking station are validated on the basis of formalized model. The result shows that the modeling and verification methods based on Term Rewriting System can be used for the verification of interlocking systems scalability, and this research provides a good reference for the formal modeling and verification of the safety-critical system.

Key words: Term Rewriting System, interlocking system, Maude, safety-critical system, model checking