Lianyi Zhang
Science and Technology on Special System Simulation Laboratory, Beijing Simulation Center, China / State Key Laboratory of Intelligent Manufacturing System Technology, Beijing Institude of Electronic System
Engineering, China
Duzheng Qing
Science and Technology on Special System Simulation Laboratory, Beijing Simulation Center, China / State Key Laboratory of Intelligent Manufacturing System Technology, Beijing Institude of Electronic System
Engineering, China
Lixin Yu
State Key Laboratory of Intelligent Manufacturing System Technology, Beijing Institude of Electronic System
Engineering, China
Mo Xia
Software School, Tsinghua University, Beijing, China
Han Zhang
State Key Laboratory of Intelligent Manufacturing System Technology, Beijing Institude of Electronic System
Engineering, China
Zhiping Li
State Key Laboratory of Intelligent Manufacturing System Technology, Beijing Institude of Electronic System
Engineering, China
Download article
http://dx.doi.org/10.3384/ecp17142273Published in: Proceedings of The 9th EUROSIM Congress on Modelling and Simulation, EUROSIM 2016, The 57th SIMS Conference on Simulation and Modelling SIMS 2016
Linköping Electronic Conference Proceedings 142:39, p. 273-279
Published: 2018-12-19
ISBN: 978-91-7685-399-3
ISSN: 1650-3686 (print), 1650-3740 (online)
Multifunction Vehicle Bus (MVB) is a critical component in the Train Communication Network (TCN), which represents a challenging problem for model checking. Although model checking is widely used in circuit and software veri?cation, it is hardly for veri?cation of the MVB or TCN, in terms of modelling of MVB components and making appropriate speci?cation. The study described in this paper aims at evaluating and experimenting the industrial application of veri?cation by model checking, and provides a complete system modelling and speci?cation describing technique. The model of MVB consists of device model, communication model and speci?cation model translated from LSCs, a scenario description. Experiments results with SPIN checking tool illustrate effectiveness of our approach.
