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.
Formal safety verification for TTP/C network in Drive-by-wire system
2007-12-01
307812 byte
Conference paper
Electronic Resource
English
Formal verification method for safety diagnosis software
Automotive engineering | 2015
|Formal Safety Verification of Automotive Microcontroller Parts
Tema Archive | 2012
|Formal Verification Method for Safety Diagnosis Software
SAE Technical Papers | 2015
|Formal Verification of Safety-Critical Aerospace Systems
IEEE | 2023
|