Systems-on-Chips rely on the correct functioning of the communication between their components. As these systems grow more complex, so do the underlying communication networks. Simulating a network does not guarantee the entire state-space is explored, therefore formal verification methods should be used to ensure correctness of these Networks-on-Chips. This thesis uses the MaDL modelling language to model and verify liveness of networks. Although MaDL is a useful tool for the verification of networks, it lacks the capability to completely model and analyse ring networks. Therefore, MaDL is extended with a new primitive and a ring detection algorithm that cooperate to generate additional network invariants specifically for ring networks. These extensions are used in two case studies to model and verify network architecture proposals from literature. The analysed networks are TornadoNoC [10] and LIGERO [1]. In both case studies, the process of formally modelling these architectures reveals ambiguity in the original proposal papers. Both architectures turn out to contain deadlocks when modelling as close to their original proposal as possible. The results show formal modelling is a useful tool to eliminate ambiguity, but still requires improvement to allow it to scale to larger networks. The extensions to MaDL prove to be useful when modelling certain networks, but can still be improved to allow verification of a wider range of different networks.