This paper presents a new formal method, called Calculus of Real-Time Distribution, Mobility, and Interaction (CaRDMI), to specify and verify spatial and temporal behaviors of transportation systems. For specification, CaRDMI defines a map, consisting of nodes and edges with spatial and temporal constraints. The movement of a carrier or agent in the system is represented by a path on the map. Interactive constraints among carriers are represented by synchronization modes on objects at nodes, which are distinguishable features of CaRDMI from other methods. Especially, n-to-n timed synchronization constraints are noticeable. For verification, CaRDMI presents the spatial, temporal and interactive deduction rules and the spatial and temporal equivalence relations. With the rules and relations, it can be measured how two carriers or agents are temporally and/or spatially equivalent. It is another distinguishable feature of CaRDMI.