Formal Safety Modelling and Analysis of Train-to-Train Communication in Virtual Coupling Using CPN

Virtual coupling introduces a paradigm shift in railway operational and control systems by enabling decentralized coordination between multiple trains thanks to reliable Train-to-Train wireless communications. In this context, information exchanges between trains become a safety-critical aspect that must be formally analyzed. This paper presents a Coloured Petri Net-based approach for the formal modelling and safety analysis of Train-to-Train wireless Cooperative Awareness Messages exchanges in virtual coupling contexts, particularly between two trains. The proposed Coloured Petri Net model captures both system behavior and communication interaction behavior. It enables the explicit formulation of safety properties as temporal constraints on message exchanges, including bounded-delay and bounded inter-message-gap requirements. In contrast to traditional performance-oriented analysis, communication metrics such as delay, delivery ratio, and inter-message reception are regarded as evidence that is assumption-bounded and supports the satisfaction of formal safety properties, rather than serving as direct guarantees of safety. This distinction provides a structured reasoning framework aligned with railway safety standards, in which safety claims are substantiated by traceable arguments. This approach positions the Coloured Petri Net model as a formal component within the safety assurance process. It bridges the gap between system modelling, communication analysis, and safety argumentation. The results demonstrate how communication constraints influence safe train operation and provide a basis for systematically apportioning safety requirements in virtual coupling systems.