Domain modeling is an important aspect of software engineering. This paper presents our experience of modeling land transportation domain in the formal framework of Event-B. The domain exhibits interesting features, such as high levels of non-determinism, complex interactions, stringent safety properties, etc.. Time is an essential multifaceted feature of the domain. We discuss the