Abstract: Abstract: The modeling and verification is an important area in the research of cyber physical systems (CPS). By integrating physical processes, CPS has many physical properties, not in traditional software systems, which must be described in the model of CPS. In this paper, the mobility of CPS is studied. As a physical property, the mobility can describe the movement of physical entities and the flow of information in CPS. A model of CPS based on Mobile Safe Ambients is proposed in this paper, whose properties are analyzed and verified by means of ambient logic. The proposed model can describe and analyze mobility in CPS, and is suitable for applications of mobile CPS. The case study on European Train Control System (ETCS) shows the feasibility of the proposed method on the modeling and verification.