Entanglement swapping is a basic primitive in long distance quantum communications. The stochastic nature of various operations like entanglement generation and BSMs makes the entanglement swapping primitive failure prone. It is difficult to predict whether or not an entanglement swapping operation will succeed within a stipulated time. In this paper, we use Probabilistic Timed Automata (PTA) to model the experiment and analyze it through model checking. We report a proof-of-concept mechanism, opening way for the analysis of large scale quantum networks through formal methods. We also report supporting results on a quantum simulator. © 2022, Springer Nature Switzerland AG.