A Reusable Framework for Modeling and Verifying In-vehicle Networking Systems in the Presence of CAN and FlexRay

In an IVN system, electronic components are connected and communicated through multiple protocols subjected to different requirements. In practice, intelligent vehicles need to exchange data between the body control subsystem and the chassis control subsystem, usually involving both the controller area network (CAN) protocol and the FlexRay protocol. In such a system, delays and congestion of frame transmissions are more likely to happen, leading to safety issues. In this paper, following a two-stage strategy, we managed to find an appropriate abstraction to model the IVN system in the presence of both protocols. Based on the abstraction, we proposed a framework for modeling and verifying IVN systems in their design phase using timed model checking techniques. To analyze the timed properties of communications, we chose the UPPAAL as the platform. Regarding concerns of reusability, this framework was structured in such a way that it is adaptable to IVN systems with different topologies. This framework was validated by checking the communication behaviors against the protocol specifications. We constructed design models with three typical topologies and estimated the response time of frames. The reusability of this framework over different topologies was demonstrated by comparing the estimated response times against the corresponding topological characteristics.