Modelling and Analysing Dynamic Decentralised Systems

TL;DR

This paper presents a novel method for specifying and analyzing decentralised dynamic systems by combining event-based multi-process specifications with multi-facet analysis, demonstrated through mobile ad-hoc network modeling.

Contribution

It introduces a new combined approach for decentralized system analysis using Event-B, integrating abstract and specific models for facet-wise analysis.

Findings

Effective modeling of mobile ad-hoc networks demonstrated

Use of Event-B and tools B4free and ProB validated the approach

Facilitates detailed analysis of decentralized dynamic systems

Abstract

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.