Formal modeling and verification for MVB. (English) Zbl 1271.90019

Summary: Multifunction Vehicle Bus (MVB) is a critical component in the Train Communication Network (TCN), which is widely used in most of the modern train techniques of the transportation system. How to ensure security of MVB has become an important issue. Traditional testing could not ensure the system correctness. The MVB system modeling and verification are concerned in this paper. Petri Net and model checking methods are used to verify the MVB system. A Hierarchy Colored Petri Net (HCPN) approach is presented to model and simulate the Master Transfer protocol of MVB. Synchronous and asynchronous methods are proposed to describe the entities and communication environment. Automata model of the Master Transfer protocol is designed. Based on our model checking platform M\(^{3}\)C, the Master Transfer protocol of the MVB is verified and some system logic critical errors are found. Experimental results show the efficiency of our methods.


90B18 Communication networks in operations research
68Q80 Cellular automata (computational aspects)
90C35 Programming involving graphs or networks


Full Text: DOI


[1] J. JimĂ©nez, I. Hoyos, C. Cuadrado, J. Andreu, and A. Zuloaga, “Simulation of message data in a testbench for the multifunction vehicle bus,” in Proceedings of the 32nd IEEE Annual Conference on Industrial Electronics (IECON ’06), pp. 4666-4671, 2006.
[2] H. Zhiwu, Z. Sheng, G. Weihua, and L. Jianfeng, “Research and design of protocol analyzer for multifunction vehicle bus,” in Proceedings of the 7th IEEE World Congress on Intelligent Control and Automation (WCICA ’08), pp. 8358-8361, 2008.
[3] E. M. Clarke and E. A. Emerson, “Design and synthesis of synchronization skeletons using branching time temporal logic,” in Logics of Programs, vol. 131, pp. 52-71, Springer, Berlin, Germany, 1982. · Zbl 0546.68014
[4] J. P. Queille and J. Sifakis, “Specification and verification of concurrent systems in CESAR,” in International Symposium on Programming, vol. 137, pp. 337-351, Springer, Berlin, Germany, 1982. · Zbl 0482.68028
[5] C. Baier and J.-P. Katoen, Principles of Model Checking, MIT Press, Cambridge, Mass, USA, 2008. · Zbl 1179.68076
[6] R. Jhala and R. Majumdar, “Software model checking,” ACM Computing Surveys, vol. 41, no. 4, p. 21, 2009.
[7] G. Frey and L. Litz, “Formal methods in PLC programming,” in Proceedings of the IEEE International Conference on Systems, Man, and Cybernetics, vol. 4, pp. 2431-2436, 2000.
[8] P. Huber, K. Jensen, and R. M. Shapiro, “Hierarchies in coloured Petri nets,” in Advances in Petri Nets 1990, vol. 483 of Lecture Notes in Computer Science, pp. 313-341, Springer, Berlin, Germany, 1991.
[9] G. Fadin, H. Kirrmann, and P. Umiliacchi, “Rosin, railway open system interconnection network. Web technologies for railways,” in Proceedings of Automation in Transportation, 1998.
[10] P. Umiliacchi, “The role of european research in the railways modernisation process: the rosin project,” in Proceedings of the World Congress on Railway Research, pp. 63-68, 1997.
[11] I. E. Commission, et al., “IEC 61375-1,” Train Communication Network, 1999.
[12] H. Kirrmann and P. Zuber, “The IEC/IEEE train communication network,” IEEE Micro, vol. 21, no. 2, pp. 81-92, 2001. · Zbl 05097722
[13] M. Huth and M. Ryan, Logic in Computer Science: Modelling and Reasoning about Systems, vol. 2, Cambridge University Press, Cambridge, Mass, USA, 2nd edition, 2004. · Zbl 1073.68001
[14] K. Jensen, “Coloured Petri nets,” in Petri Nets: Central Models and Their Properties, vol. 254, pp. 248-299, Springer, Berlin, Germany, 1987. · Zbl 0632.68058
[15] P. Liu, G. Luo, M. Xia, and M. He, “Automatic verification of event-driven control programs: a case study,” in Proceedings of the 4th IEEE International Workshop on Advanced Computational Intelligence (IWACI ’11), pp. 249-256, 2011.
[16] K. John and M. Tiegelkamp, IEC 61131-3: Programming Industrial Automation Systems: Concepts and Programming Languages, Requirements for Programming Systems, Decision-Making Aids, Springer, 2010. · Zbl 0943.68036
[17] G. Holzmann, “The model checker spin,” IEEE Transactions on Software Engineering, vol. 23, no. 5, pp. 279-295, 1997. · Zbl 05113845
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.