From TiMo to Event-B: Event-Driven Timed Mobility

Mobile distributed systems involve specific aspects such as migration, communication and concurrency, usually under temporal constraints. In this paper, we deal with formal modelling of timed migrating and communicating processes, as provided by the TiMo calculus. In this framework, mobile processes can move between different locations and communicate when collocated, all this happening in the presence of local timers. Our contribution is a general framework for reasoning about systems specified using TiMo. We use the Event-B modelling method as the target for translating TiMo specifications. Subsequently, we utilise the supporting Rodin platform of Event-B to verify system properties using the embedded theorem-provers and model checkers. The main feature of our encoding include a generic model capturing the syntax and semantics of TiMo, together with a concrete model corresponding to each specific TiMo specification. We illustrate our approach by a non-trivial example featuring different concepts of TiMo.