Digital infrastructures, grids, and networks heavily rely on Cyber-Physical Systems (CPSs) endpoints in a context of mobile computing, referred to as mobile CPSs, including applications such as smart cities, intelligent transportation systems, and unmanned vehicles. Most of such systems are safety-critical, i.e., any error may result in catastrophic consequences. Mobile CPSs represent a novel computing paradigm, and their inherent complexity and interdisciplinary nature pose significant challenges to system design beyond the limits of state-of-the-art separation of concerns. Model-Based Design (MBD) is a key approach to mitigate the complexity of safety-critical systems. However, it lacks adequate modeling and analysis techniques to tame mobile CPSs. To address this gap, this paper proposes an extension of sequence diagrams, as found in SysML/UML, to facilitate an accurate, graphical representation of the deeply-coupled mobile, parallel, and hybrid behaviors (i.e., the entangled interplay of discrete and continuous behaviors). To ensure the correctness of the designed models, we propose a set of transformation rules that convert the (graphical and hence, by nature, informal) extended sequence diagram to a formal representation using the hybrid \(\pi \) -calculus, thereby enabling formal verification using, e.g., bisimulation-based model checking. Finally, we provide a case study where we employ extended sequence diagrams to model the scenario of the handover protocol of a train control system and formalize it into a hybrid \(\pi \) -calculus model using the proposed transformation rules.