# ATWin: An Improved and Detailed Startup Model of TTP/C
## 1 Introduction  
The cyber-physical system (CPS) represents a new generation of intelligent systems that integrate computing, communication, and control, enabling organic interactions between humans and the physical environment. The time-triggered architecture (TTA) [1; 2; 3] is a general design framework for CPS that offers higher reliability, determinism, and maintainability compared to traditional event-triggered architecture [4]. It has been extensively adopted in various embedded real-time industry domains, particularly in aerospace and automotive electronics [5; 6; 7; 8]. TTP/C (Time-Triggered Protocol Class C) [6; 9; 10; 11; 12], which is based on TTA, has become the primary communication protocol for automotive networks that cater to the requirements of the next generation of real-time systems [4]. Notably, TTP/C is the first fully time-triggered communication protocol standardized by the Society of Automotive Engineers (SAE). This basic standard for TTP/C is named AS6003 (Aerospace Standard 6003) [13]. TTA establishes a unified global time base (GTB) within its system, which triggers a set of services such as task scheduling and message processing periodically to ensure that all nodes in the system work synchronously. The startup service [14] is one of the most significant services of TTP/C, as it is responsible for transforming the TTP/C cluster from an asynchronous state to a synchronous state within a limited time. This service should have strong fault-tolerance capability and a strict upper bound of startup time. The key points [15] of startup include how to reduce the startup time, verify the validity of the startup model, and determine the upper bound of the startup time. There are three issues that need to be addressed in the startup of TTP/C. Firstly, as the top-level design standard, the description of AS6003 [13; 16] lacks details that should be considered in actual implementation. The gap between the standard and its implementation need be bridged when the standard startup model outlined in AS6003 is put into practice. Secondly, the standard startup model in AS6003 mandates that all cold-start nodes shall unconditionally discard the first valid cold-start frame addressing the startup multi-clique problem [17], i.e., the well-known split-brain problem in the distributed system. Its contention-eliminating mechanism works; however, we find that the first valid cold-start frame does not need discarding at some scenarios to speed up the startup. Thirdly, the existing research [18; 19; 20] utilize the model checking methods to verify the standard startup model of AS6003 with limited nodes (i.e., ten or fewer). The correctness of the startup model with arbitrary number of nodes has not been proved yet. In addition, the upper time bound of the startup with any number of nodes has not not covered for AS6003 and existing studies [14; 21; 22; 23], where the upper bound is essential for performance assessment and fault diagnosis of the startup model. To address these issues, this paper proposes a detailed and improved startup model for TTP/C called ATWin (Arrival Time Window). We carefully analyze the missing details to fill the gap between the standard startup model of AS6003 and its implementation. Furthermore, a contention-detecting strategy is added to the ATWin model in order to reduce the startup time. ATWin selectively retains the first valid cold-start frame under certain conditions, while the AS6003's startup model unconditionally discards the first valid cold-start frame. Hence, ATWin can speed up the startup phase in some cases. We formally analyze the upper bound of time needed by ATWin to synchronize a cluster with an arbitrary number of nodes and prove the validity of ATWin through formal deduction, of which the exhaustive model checking methods fail to perform.