Model checking of TTCAN protocol using UPPAAL

Abstract

Recent years, vehicles are becoming more and more intelligent and automatic. Some experts estimate that more than 80% of all current innovations within vehicles are based on distributed electronic systems. The critical parts of such systems are the services provided by the underlying distributed control networks. TTCAN is the extension of the standard Controller Area Network (CAN), which is the most widely adopted in-vehicle network. As the complexity of TTCAN protocol, formal verification is the best choice to verify the specification correctness of TTCAN protocol. The previous researches are only able to verify the models of TTCAN protocol with no more than three nodes. If there are four nodes in the model, it meets two problems: state space explosion and magnanimous verification time. This paper proposes a novel method and the model of TTCAN protocol with 4 nodes can be verified. TTCAN is the extension of the standard Controller Area Network (CAN), which is the most widely adopted in-vehicle network.