Event-based mobility modeling and analysis

Mobility is a critical issue that must be considered during the modeling and analyzing of a mobile system. At a high abstract level, event-based models can directly specify a mobile system without the introduction of additional mechanisms. In this article, we first propose two types of special events, entering and exiting an ambient, as movement events. Next, based on the movement events, we introduce the notion of a movement path and propose a feasible movement criterion (deciding whether a given movement path of a mobile object (agent) is feasible or not in terms of spatiotemporal topological relationships of ambients). Then, we investigate how a message movement-based communication model represents synchronous communication, asynchronous communication, and broadcast communication in a unified way. Finally, we use movement event sequences to discuss the exclusivity of ambients (an ambient only allows one mobile object to occupy (enter) it at any moment) and show that a priority scheduling control policy can guarantee exclusivity. Accordingly, we propose a correct movement criterion-that is, a correct movement path is feasible and satisfies the exclusivity of ambients. Case studies demonstrate these results.