We provide an overview of recent work on Team Automata, which describe networks of automata with input and output actions, extended with synchronisation policies guiding how many interacting components can synchronise on a shared input/output action. First, we briefly revisit this notion of synchronisation in other well-known concurrency models, such as Reo, BIP, Choreography Automata, and Multiparty Session Types. Then we introduce Featured Team Automata, which support variability by describing families of concrete product models for specific configurations determined by feature selection. Given a (featured) team automaton one can reason over communication-safety properties, like receptiveness (sent messages must be received) and responsiveness (pending receives must be satisfied), but doing so product-wise quickly becomes impractical. Therefore, we lift these notions to the level of family models and show how to identify such communication properties. However, the purely semantic nature of communication properties is a serious burden in practice, making it challenging to automatically verify such properties in concrete cases: one has to go through all reachable states of networks of interacting automata with large state spaces and check compliance for all requirements at each state. We present a solution by providing the first logical characterisation of communication properties for team automata (and subsumed models) using test-free propositional dynamic logic and, subsequently, using this characterisation to actually verify communication properties by using available model-checking tools for dynamic logic. An open-source prototypical tool supports the developed theory, using a transformation to interact with the mCRL2 toolset for model checking. Finally, we address realisability of team automata, i.e., how to infer a network of interacting automata from a global specification, taking into account that this realisation should satisfy exactly the same properties as the global specification. We identify and compare two variants to realise such global models, both relying on bisimulation equivalence. Then we investigate, for both variants, realisability conditions to be checked on global models. We propose a synthesis method for the construction of realisations by grouping locally indistinguishable states. The theory is accompanied by an open-source prototypical tool that implements realisability checks and synthesises realisations.