×

Formal verification of safety protocol in train control system. (English) Zbl 1420.68139

Summary: In order to satisfy the safety-critical requirements, the train control system (TCS) often employs a layered safety communication protocol to provide reliable services. However, both description and verification of the safety protocols may be formidable due to the system complexity. In this paper, interface automata (IA) are used to describe the safety service interface behaviors of safety communication protocol. A formal verification method is proposed to describe the safety communication protocols using IA and translate IA model into PROMELA model so that the protocols can be verified by the model checker SPIN. A case study of using this method to describe and verify a safety communication protocol is included. The verification results illustrate that the proposed method is effective to describe the safety protocols and verify deadlocks, livelocks and several mandatory consistency properties. A prototype of safety protocols is also developed based on the presented formally verifying method.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata
93C83 Control/observation systems involving computers (process control, etc.)

Software:

SPIN; vUML
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Heimdahl, M. P. E., Safety and software intensive systems: challenges old and new, 137-152 (2007), Washington · doi:10.1109/FOSE.2007.18
[2] Esposito R, Sanseviero A, Lazzaro A, et al. Formal verification of ERTMS euroradio safety critical protocol. In: Proceedings of FORMS 2003. Budapest: IEEE Computer Society, 2003. 21-29
[3] Diao Y F, Wang B D. Risk analysis of flood control operation mode with forecast information based on a combination of risk sources. Sci China Tech Sci, 2010, 53(7): 1949-1956 · doi:10.1007/s11431-010-3124-3
[4] Chu Y Y, Zhang H, Shen S F, et al. Development of a model to generate a risk map in a building fire. Sci China Tech Sci, 2010, 53(10): 2739-2747 · doi:10.1007/s11431-010-4063-8
[5] Xu T H, Tang T, Gao C H, et al. Dependability analysis of the data communication system in train control system. Sci China Tech Sci, 2009, 52(9): 2605-2618 · Zbl 1177.90075 · doi:10.1007/s11431-009-0183-4
[6] Gronbaek, J.; Madsen, T. K.; Schwefel, H. P., Safe wireless communication solution for driver machine interface for train control systems, 208-213 (2008), Cancun
[7] Zhang Y, Tang T, Yan F. Study on model for analysis of CBTC data communication system (DCS) and its application (in Chinese). J China Railway Soc, 2011, 33(5): 60-65
[8] Sinha P, Ren D Q. Formal verification of dependable distributed protocols. Inf Software Technol, 2003, 45(12): 873-888 · doi:10.1016/S0950-5849(03)00066-1
[9] Clarke E M, Wing J M. Formal methods: state of the art and future directions. ACM Computing Surveys, 1996, 28(4): 626-643 · doi:10.1145/242223.242257
[10] Lee J H, Hwang J G, Park G T. Performance evaluation and verification of communication protocol for railway signaling systems. Computer Standards & Interfaces, 2005, 27(3): 207-219 · doi:10.1016/S0920-5489(04)00097-2
[11] Lee J D, Jung J I, Lee J H, et al. Verification and conformance test generation of communication protocol for railway signaling systems. Computer Standards & Interfaces, 2007, 29(2): 143-151 · doi:10.1016/j.csi.2006.03.001
[12] Lee J H, Hwang J G, Shin D, et al. Development of verification and conformance testing tools for a railway signaling communication protocol. Computer Standards & Interfaces, 2009, 31(2): 362-371 · doi:10.1016/j.csi.2008.05.011
[13] Katsaros P. A roadmap to electronic payment transaction guarantees and a Colored Petri Net model checking approach. Inf Software Technol, 2009, 51(2): 235-257 · doi:10.1016/j.infsof.2008.01.005
[14] Sinha, P.; Suri, N., Modular composition of redundancy management protocols in distributed systems: an outlook on simplifying protocol level formal specification and verification, 255-263 (2001), Phoenix
[15] Sinha, P.; Suri, N., On simplifying modular specification and verification of distributed protocols, 173-181 (2001), Boca Raton, Florida
[16] Ouzzif M, Erradi M, Mountassir H. Description of a teleconferencing floor control protocol and its implementation. Eng Appl Artif Intel, 2008, 21(3): 430-441 · doi:10.1016/j.engappai.2007.11.003
[17] Schäfer T, Knapp A, Merz S. Model checking UML state machines and collaborations. Elec Notes Theor Comp Sci, 2001, 55(3): 357-369 · doi:10.1016/S1571-0661(04)00262-2
[18] Inverardi, P.; Muccini, H.; Pelliccione, P., Automated check of architectural models consistency using SPIN, 346-349 (2001), Los Alamitos · doi:10.1109/ASE.2001.989826
[19] Alfaro, L.; Henzinger, T. A., Interface automata, 109-120 (2001), Vienna
[20] Alfaro, L. D.; Henzinger, T. A., Interface theories for component-based design, 148-165 (2001), Tahoe City, CA · Zbl 1050.68518
[21] Jin, Y.; Esser, R.; Lakos, C.; etal., Modular analysis of dataflow process networks, 184-199 (2003), Warsaw · Zbl 1032.68110
[22] Chakrabarti, A.; Alfaro, L.; Henzinger, T.; etal., Interface compatibility checking for software modules, 428-441 (2002), Copenhagen · Zbl 1010.68505 · doi:10.1007/3-540-45657-0_35
[23] Chakrabarti, A.; Alfaro, L. D.; Henzinger, T. A.; etal., Synchronous and bidirectional component interfaces, 414-427 (2002), Copenhagen · Zbl 1010.68518 · doi:10.1007/3-540-45657-0_34
[24] Lee E A, Xiong Y, Behavioral types for component-based design. Technical Report No. UCB/ERL M02/29, Berkeley, USA, 2002
[25] Kapus T. Using mobile TLA as a logic for dynamic I/O automata. IEICE Trans Inf Syst, 2009, 92(8): 1515-1522 · doi:10.1587/transinf.E92.D.1515
[26] Refsdal A, Stølen K. Extending UML sequence diagrams to model trust-dependent behavior with the aim to support risk analysis. Sci Comp Progr, 2008, 74(1-2): 34-42 · Zbl 1162.68355 · doi:10.1016/j.scico.2008.09.003
[27] Medvidovic N, Rosenblum D S, Redmiles D F, et al. Modeling software architectures in the Unified Modeling Language. ACM Trans Software Eng Methodol, 2002, 11(1): 2-57 · doi:10.1145/504087.504088
[28] Li, X. D.; Hu, J.; Bu, L.; etal., Consistency checking of concurrent models for scenario-based specifications, 1171-1180 (2005), Berlin
[29] Holzmann G J. The model checker SPIN. IEEE Trans Software Eng, 1997, 23(5): 279-295 · doi:10.1109/32.588521
[30] Wang Y, Wei J, Wang Z Y. Model checking distributed control systems based on software architecture (in Chinese). J Software, 2004, 15(6): 823-833 · Zbl 1066.93035
[31] Hu J, Yu X F, Zhang Y, et al. Checking component-based designs for scenario-based specifications (in Chinese). Chin J Comp, 2006, 29(4): 513-525
[32] Bharadwaj R, Heitmeyer C L. Model checking complete requirements specifications using abstraction. Autom Software Eng, 1999, 6(1): 37-68 · doi:10.1023/A:1008697817793
[33] Mikk, E.; Lakhnech, Y.; Siegel, M.; etal., Implementing statecharts in PROMELA/SPIN, 90-101 (1998), Florida
[34] Lilius, J.; Paltor, I. P., VUML: a tool for verifying UML models, 255-258 (1999), Florida · doi:10.1109/ASE.1999.802301
[35] IEC, IEC 62280-2, Railway applications-communication, signaling and processing systems-part 2: safety-related communication in open transmission systems. New York: IEC, 2001
[36] ERTMS/ETCS UNISIG Subset-037: Euroradio FIS. http://www.era.europa.eu/Document-Register/Documents/Subset-037
[37] Zhang Y, Zhao X Q, Zheng W, et al. System safety property-oriented test sequences generating method based on model checking. WIT Trans Built Environ, 2010, 144(1): 747-759 · doi:10.2495/CR100681
[38] Zhang Y, Tang T, Ma L C, et al. Modeling and simulation of the security communication protocol based on the switched Ethernet (in Chinese). J China Railway Soc, 2010, 32(3): 43-48
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.