LAUSR

TTP/C (Time-Triggered Protocol Class C) is a mainstream communication protocol commonly utilized in cyber–physical systems within the aerospace and automotive industry. Unfortunately, when it comes to the startup model, there are three issues in the standard of TTP/C (namely AS6003). Firstly, AS6003 only mentions a high-level specification, which leads to a gap between the standard and its implementation. Secondly, the standard startup model in AS6003 aggressively handles the multi-clique problem by dropping the first valid frame unconditionally without a contention-detecting mechanism, resulting in additional time consumption in some types of contention scenarios. At last, there is lack of the formal verification for the validity of the standard startup model with an arbitrary number of nodes and the formal derivation of its upper bound of startup time. To address these limitations, we propose a detailed and improved startup model named ATWin based on AS6003. It not only bridges the gap between the top-level standard and its implementation by supplementing the undefined details, but it also enhances the efficiency of the startup time by adding a contention-detecting strategy to the standard startup model. The ATWin model is developed as an open-source implementation for TTP/C’s startup. We also formally demonstrate the validity of ATWin and deduce its upper bound of startup time with an arbitrary number of nodes in this paper.