VeRV: A temporal and data-concerned verification framework for the vehicle bus systems

As a part of the international standard IEC 61375, the multifunction vehicle bus (MVB) has been used in most of the modern train control systems. It is highly desirable to check the temporal properties of the data transmitted on the bus. However, we are not aware of any published work on this problem. We proposed VeRV, the first temporal and data-concerned verification framework for the vehicle bus systems. A domain-specific language, called VeSpec, is proposed to specify the packet formats and the desired properties. The language is expressive, modular and easy to use. Given a VeSpec script, the VeRV allows automatic generation of runtime analyzer. We have applied our technique to a real tube train system and succeeded in diagnosing a real failure in this system. The industry application illustrates the effectiveness and efficiency of our technique.