We present and formalize Mob _adtl, a model for network-aware applications, extending the Oikos-adtl temporal-logic based approach to the specification and verification of distributed systems. The model supports strong subjective mobility of agents under the control of stationary guardians. Communications are based on asynchronous message passing. The approach exploits the notions of coordination and refinement to deal separately with the specification of functional issues in the agents, and with the specification of coordination policies, e.g. security, routing, etc., in the guardians. The goal is to specify mobile agents as independently as possible of the requirements related to the other facets of distribution. The specification of an application is obtained by instantiating the general model, refining it along different dimensions corresponding to the different aspects of interest, and finally composing the refinements. The main advantage, besides the increased flexibility of the specification process, is that it is possible to specify rich coordination policies incrementally, while the functional units remain relatively simple. We use Mob _adtl to specify a simple electronic commerce application, paying particular attention to the incremental specification of the policies. We show how refined policies lead to stronger system properties.