Design And Implementation Of Runtime Verification Tool For Vehicle Bus Network

The data transmitted on MVB(Multifunction Vehicle Bus) contains information about the state of device in the train. To keep the train safe and comfortable, the data is required to satisfy some constraints(or properties). These constraints may be constraints on packet order, constraints on packet length and constraints on the value of some data in the packets. It is of much significance to monitor whether these properties are satisfied. Monitoring the correctness of data can help to find faults in device as early as possible and guarantee that the device work normally.With the problem of monitoring the correctness of MVB data as background, this paper explores, designs and develops a runtime verification tool for train properties-VeRV(Runtime Verification for Vehicle bus systems), aiming at providing a general solution for similar problems. VeRV consists of two parts: VeSpec(Specification of Vehicle bus) language and VeRV engine. The basic idea of VeRV is to express the verification problem with VeSpec, parse the script and generate monitor programs with VeRV engine.The only thing users need to do is writing verification scripts and deploying monitors. By providing a language, VeRV provides reusability of script defining variables, events and properties, which makes the solution more general.The contributions of this paper include:1. The paper proposes one runtime verification tool for data on train bus- VeRV. The paper gives an introduction to its functions and system design. One example is used to illustrate VeRV ’s usage and workflow.2. The paper proposes one domain-specific language- VeSpec, to describe the formats of packets and temporal properties. In VeSpec, the definition of properties is decomposed into three levels: property, event and variables. The three-level design connects packet data and ptLTL(past time Linear Temporal Logic) properties, and also guarantees the reusability of scripts.3. The paper introduces our application of VeRV to MVB data analysis. In this experiment, several properties are elaborated and verified at runtime. The experimental results show the e?ectiveness of VeRV tool on data verification and faults diagnosis.