Formal Modeling and Verifying the TTCAN Protocol from a Probabilistic Perspective

The time-triggered CAN (TTCAN) protocol has been widely used in the automotive industry to fulfil the safety and real-time requirements of the application. As an extension of the standard CAN protocol, the TTCAN protocol aims to guarantee a safe and deterministic communication by introducing time-triggered messages with respect to a global synchronized time, which are scheduled in independent transmission windows within the system matrix. However, the new features bring more difficulties in designing and verifying the reliable applications in the TTCAN network. In this paper, we first present a formal probabilistic model of the TTCAN protocol with a consideration of its novel features. A TTCAN system consisting of three parts, i.e., a system matrix, an arbitration and some nodes, is modeled as discrete Markov chains model. Furthermore, five probabilistic properties are described and verified in the probabilistic model checker tool PRISM. Our work gives a quantitative analysis method for the given requirements, which facilitates the designers to a formal understanding of TTCAN protocol.