Formal safety verification for TTP/C network in Drive-by-wire system

TTP/C is a member of the time-triggered protocol (TTP) family that satisfies Society of Automotive Engineers Class C requirements for hard real-time fault-tolerant communication. As a communication network designed for safety-critical system, it is essential to verify its safety depending on formal methods. We investigate the fault-tolerant and fault-avoidance strategies of TTP/C network used in Drive-by-wire system, with Markov modeling techniques, and evaluate the failure rate subject to different failure modes, taking into account both transit and permanent physical failures. Generalized Stochastic Petri Net (GSPN) is selected to model concurrency, non-determinism properties and calculate Markov model automatically. A model with 157 states and 78 transitions is built. The result of experiments shows that failure probability of TTP/C network in 7-nodes DBW system varies from 10^-6 to 10^-10 with different configuration. And diagnose mistakes are proved to be a critical factor for the success of membership service.