Title:
Model Checking of Automotive System in the Presence of Multiple Communication Protocols

Speaker:
GUO, Xiaoyun (JAIST)

Abstract:
Automotive system is a real-time distributed control system to realize a variety of functions with electronic components in the vehicle. These components connected by buses, and communicate with each other following communication protocol. CAN, LIN, FlexRay and MOST are the most common communication protocol, which are suitable for different functions of the control system. Automotive system consists of multiple subsystems with different communication protocols. Communication between subsystems is extremely complicated. It is difficult to guarantee the time properties. The timing of message transmission is affected by gateway and the protocols. We proposed a framework to verify the communication of automotive systems in the presence of multiple communication protocols. There are two kinds of subsystems following different protocols, which are connected by a gateway. Each subsystem is abstracted as an environment with arbitrary topology and the number of nodes, and need to send messages to the other kind of subsystem. The message can be sent at any time. The gateway contains the two kinds of protocols. It can not only connect the two environments, and be able to convert the protocols. The gateway receives messages from an environment and forwards messages to the other environment. Based on the framework, we construct a simple automotive system model with CAN and FlexRay protocol in UPPAAL model checker, including two environment modules, two protocol modules and gateway module. We abstract behaviors related transmitting messages and timing synchronization from protocol specifications to establish the protocol module. Three properties are verified to illustrate following results. The system is deadlock free, but the capability of verification is limited depend on the number of messages. The highest priority of the message always can be sent in the simple system. Other messages may be lost in the gateway because of transmission delay and the randomness of sending messages from CAN and FlexRay subsystem.