We introduce a method to specify and analyse decentralised dynamic systems;
the method is based on the combination of an event-based multi-process system
specification approach with a multi-facet analysis approach that considers a
reference abstract model and several specific ones derived from the abstract
model in order to support facet-wise analysis. The method is illustrated with
the modelling and the analysis of a mobile ad-hoc network. The Event-B
framework and its related tools B4free and ProB are used to conduct the
experiments.