## 4 Results
### Formal Model  
As presented in [23], the formal model of the protocol outlines several critical transitions that are pivotal for understanding the behavior and potential vulnerabilities of OT communication systems. These identified critical transitions occur when there is no defined behavior for the protocol's state, i.e., a potential timeout situation without a protocol requirement for timeout handling. These critical transitions are identified based on the protocol's response patterns and the potential for error states, particularly in scenarios where devices fail to respond as expected. As we have shown in [23], the Modbus protocol is comprises a number of states and state transitions. In total, there are 787 states and 11,385 transitions that result from the formal model development. Out of these, there are 5799 state transitions that are critical transitions. However, after model optimization as described in our prior work, we can collapse the vast majority of the states to arrive at 62 total reduced states. The same trend is apparent when reviewing specific interactions, such as the Read Coils functionality, which is comprised of 18 states and 92 transitions, 16 of which are critical transitions. Model reduction arrives at a total of four reduced states. The number of critical transitions may initially appear large, suggesting that a wide array of conditions requires investigation. However, a deeper analysis of the state diagram in Figure 3 reveals that many of these transitions are concentrated around a specific critical state--State 0--where a valid packet is not returned, a scenario that can trigger multiple different failure modes. These failure modes may indicate failure during normal operation or under a cyberattack. State 0, as depicted in Figure 3, acts as a central point of failure in the protocol's operation, where the lack of a valid response from the receiving device leads to a cascade of critical transitions. This state is particularly important because it represents a condition where the DUT does not acknowledge or process the incoming packet, which can result from various issues, including network congestion, packet loss, or protocol misinterpretation. The concentration of transitions in this state indicates that a significant portion of the protocol's vulnerabilities may be tied to handling such scenarios. Analyzing these transitions is crucial for identifying weaknesses in error handling, timeout management, and recovery mechanisms, all of which are vital for maintaining the reliability and security of OT communication systems. Upon further examination, the transitions in State 0 also suggest that the protocol's ability to handle invalid or missing packets is a critical factor in maintaining overall network reliability. If the protocol does not account for these failure modes with appropriate corrective actions, such as retransmission or error recovery, the network may experience prolonged periods of instability or even total failure. This highlights the importance of formal modeling in identifying these weak points early in the design or deployment process, allowing for targeted improvements in the protocol's error-handling mechanisms. Although Modbus is widely adopted due to its open standard and simplicity, certain critical transitions can still significantly impact device implementations, particularly in the context of cyberattacks. These transitions are often challenging to detect in distributed systems, where each device may have distinct operational requirements and serve diverse applications. Additionally, the variability in protocol implementations across different  
Figure 3: States of Modbus formal model-single transaction (61 states). vendors, or even within products from the same vendor, complicates the identification of critical transitions, deadlocks, or livelocks. Addressing these issues is essential for developing a more resilient and compliant protocol ecosystem.