Cyber-physical systems (CPSs) are the next generation of embedded systems that heavily interact with each other and their environment to fulfill advanced functionality. The coordination between them may be realized in software by means of asynchronous message communication. Due to the criticality of these systems, a formal verification like model checking is required in order to guarantee the functional correctness of the software. However, the input language of a model checker does not directly support domain-specific aspects such as asynchronous communication. Thus, a software engineer has to specify them using numerous model elements. This is highly complex and, thus, error-prone. This thesis presents a model-driven method for the domain-specific specification and fully automatic verification of the message-based coordination of CPSs. By using this method, the software engineer can model the coordination in a compact manner and does no longer need to understand how his specification is represented at the level of the model checker. Consequently, this thesis makes the complexity for the software engineer more manageable. Concerning the specification of such a coordination, this thesis defines a domain-specific language called Real-Time Coordination Protocols (RTCPs). In addition, it introduces a domain-specific language for the specification of verification properties and design patterns for RTCPs to reduce the number of modeling errors.