Modeling CAN network using PRISM

Although the probabilistic model checking tool called PRISM had been applied in many communication systems, such as wireless local area network, Bluetooth, and ZigBee, the technique is not used in a controller area network (CAN). In this paper, we use PRISM to model the mechanism of priority messages for CAN because the mechanism lets CAN as leader in serial communication for automobile and industry control. Through modeling CAN, it is easy to analysis the characteristic of CAN for helping the development of security and efficiency for automobile. The Markov chain model helps us to model the behaviour of priority messages. According to the results of analysis and simulation, the high-priority messages have better throughput performance while low-priority messages have the potential to lose transmission when CAN traffic is higher.