# ATWin: An Improved and Detailed Startup Model of TTP/C
## 4 Formal Demonstration of the Validity of the ATWin Model
### The Ability of Contention Eliminating  
Based on the above analysis, the reliability of the first frame received by a receiving node is uncertain, as it may activate its receiver at any time. Therefore, the first round of startup is always considered as contention according to AS6003. Theorem 1 shows that the sending times of the concurrent startup nodes are always within a limited time interval. The receiving nodes should perform the priority back-off strategy at the end of ATW according to the setting of the priority back-off timer. All sending nodes should try to execute a specific TDMA round after sending a cold-start frame, to determine whether they are in the majority clique. According to the AS6003, the sending node needs to enter the PRP phase at the end of ATW, and they should start clique detection in the PSP phase of the next sending slot. This section details the effectiveness of using the ATW to eliminate contention. The reliability of the first frame received by the receiving node is uncertain, as it may activate its receiver at any time. Consequently, the initial round of startup is inherently contentious. Theorem 1 establishes that the transmission times of concurrent startup nodes are uniformly distributed within a finite time interval. The receiving nodes are advised to implement a priority back-off strategy at the conclusion of the adaptive transmission window (ATW) according to the configured priority back-off timer. Following transmission \begin{table}
\begin{tabular}{l l l} \hline \hline
**Refinements** & **Standard Model** & **ATWin** \\ \hline Behaviors of cold-start sending nodes when bus contention occurs & Undefined & ATW with lower bound \\ \hline Behaviors of listening nodes at startup time & Drop off the first valid frame forcedly & Drop off the first valid frame according to the contention-detecting status in ATWin \\ \hline Applicative system topology & Undefined & Bus topology, but star topology is also applicative in some cases \\ \hline Formal definition of concurrent startup & Undefined & Formally defined \\ \hline Timing guarantee and behaviors definition after the frame reception at startup time & Vague & Formally defined \\ \hline Proof of correctness & Model checking with limited nodes with fault tolerant cases & Formal analysis with arbitrary number of nodes under fault free cases \\ \hline Startup upper bound & Not given & Formal expression \\ \hline \hline \end{tabular}
\end{table} 
Table 6: The main differences between the standard startup model and our ATWin startup model. of a cold-start frame, all sending nodes should endeavor to execute a particular time division multiple access (TDMA) round to determine whether they belong to the majority clique. Per the AS6003 specification, sending nodes are required to enter the primary redundant port (PRP) phase at the end of ATW, and to initiate clique detection during the primary standby port (PSP) phase of the succeeding sending slot. This section elucidates the efficacy of leveraging ATWin to mitigate contention. For any node \(i\) and node \(j\) belonging to the union of \(\mathsf{S}_{l}(n)\) and \(\mathsf{S}_{l}(n)\), the absolute value of the difference between their decision time points is less than or equal to \(\left(\Delta_{prop}+\Delta_{PRP}\right)\) in the \(n\)-th round of startup (see Appendix B for detailed proof). \[\left|T^{i}_{start}(n)-T^{j}_{start}(n)\right|\leq\Delta_{prop}+\Delta_{PRP} \tag{17}\]  
If contention occurs when the bus is occupied at the \(n\)-_th_ round of startup, all nodes of set \(S_{l}(n)\) will obtain the sending authentication, and all the nodes of set \(S_{l}(n)\) can detect the contention. However, the nodes in set \(S_{z}(n)\) may try to start during the contention and enter the listening state. They may happen to receive one complete valid frame. They should discard the complete valid frame received during this period and set the contention status flag to be true.