Abstract
In order to do formal verification of interlocking system, which is complicated but safety critical, we choose formal specification language Maude for modeling and verification based on membership equational logic and rewriting logic. In this chapter, a method is proposed to show how the initial state can be modeled and contains important information of specific interlocking system. And a case of Tongji Test Line is reported to illustrate this method in detail. The verification results show that Maude can be applied to formal object-oriented specification and model checking of railway interlocking system successfully using the proposed modeling method.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Chen, B., & Wu, F. (2002). Research on formal models of railway signal interlocking logics. Journal of The China Railway Society, 24(6), 50–54.
Ji, G. (2011). The Formal analysis of security protocols based on Maude. Xi’an: Xidian University.
Eker, S., Meseguer, J., & Sridharanarayanan, A. (2004). The Maude LTL model checker. Electronic Notes in Theoretical Computer Science, 71, 162–187.
Mccombs, T. (2003). Maude 2.0 primer. http://maude.cs.uiuc.edu
Clavel, M., Duran, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., et al. (2011). Maude manual (version 2.6). http://maude.cs.uiuc.edu
Clavel, M., Duran, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., et al. (2002). Maude: Specification and programming in rewriting logic. Theoretical Computer Science, 285(2), 187–243.
Zhang, M. (2007). On the model checking of SN P systems based on rewriting logic. Shanghai: Shanghai Jiao Tong University.
Denker, G. (1998). From rewrite theories to temporal logic theories. Electronic Notes in Theoretical Computer Science, 15, 105–126.
Meseguer, J. (1999). Research directions in rewriting logic. Computational Logic. NATO ASI Series, 165, 347–398.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Ma, R., Xu, Z., Chen, Z., Zhang, S. (2014). Initial State Modeling of Interlocking System Using Maude. In: Wong, W.E., Zhu, T. (eds) Computer Engineering and Networking. Lecture Notes in Electrical Engineering, vol 277. Springer, Cham. https://doi.org/10.1007/978-3-319-01766-2_36
Download citation
DOI: https://doi.org/10.1007/978-3-319-01766-2_36
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-01765-5
Online ISBN: 978-3-319-01766-2
eBook Packages: EngineeringEngineering (R0)