Real-time migration properties of rTiMo verified in Uppaal

Abstract

This paper extends the TiMo family by introducing a real-time version named rTiMo. The rTiMo processes are able to move between different locations of a distributed environment, and communicate locally with other processes. Real-time constraints are used to control migration and communication in a real-time distributed system. In order to verify several properties of complex mobile systems described in rTiMo, we establish a relationship between rTiMo networks and a class of timed safety automata. The relationship allows the verification of temporal properties of real-time migrating processes using Uppaal capabilities. In particular, we check whether certain configurations are reached, and that certain timing constraints hold for an entire complex evolution. © 2013 Springer-Verlag.