The theory of Communicating Sequential Processes going back to Hoare and Roscoe is still today one of the reference theories for concurrent specification and computing. In 1997, a first formalization in Isabelle/HOL of the denotational semantics of the Failure/Divergence Model of CSP was undertaken; in particular, this model can cope with infinite alphabets, in contrast to model-checking approaches limited to finite ones. In this paper, we extend this theory to a significant degree by taking advantage of more powerful automation of modern Isabelle version, which came even closer to recent developments in the semantic foundation of CSP. More importantly, we use this formal development to analyse a family of refinement notions, comprising classic and new ones. This analysis enabled us to derive a number of properties that allow to deepen the understanding of these notions, in particular with respect to specification decomposition principles in the infinite case. Better definitions allow to clarify a number of obscure points in the classical literature, for example concerning the relationship between deadlock- and livelock-freeness. As a result, we have a modern environment for formal proofs of concurrent systems that allow to combine general infinite processes with locally finite ones in a logically safe way. We demonstrate a number of verification-techniques for classical, generalized examples: The CopyBuffer and Dijkstra’s Dining Philosopher Problem of an arbitrary size.