Verification of Mobile Ad hoc Network Processes with Data

Verification of Mobile Ad hoc Network Processes with Data

Fatemeh Ghassemi


Topology-dependent behavior of wireless communication makes the modeling and verification of Mobile Ad hoc Networks (MANETs) more complicated. Reliable Restricted Broadcast Process Theory (RRBPT) was introduced to specify and analyze MANETs in an algebraic approach. Constrained Action Computation Tree Logic (CACLT), interpreted over the semantics of RRBPT, allows to specify topologydependent properties of MANETs. However, model checking of CACTL formulae is restricted to MANETs with a small number of nodes or finite datatypes. Having an algebraic specification, the problem of model checking of CACTL properties can be reduced to solving Boolean equations, as an intermediate formalism. This technique has been followed in the mCRL2 toolset to verify -calculus properties extended with data. Having a sound translation from RRBPT to mCRL2, we can use its toolset to verify data-dependent properties of MANET processes with infinite state, data-dependent behaviors. By treating the topology-dependent behavior of CACTL modals as data, we can also verify topologydependent behavior of MANETs. To this aim, we provide a sound translation from CACTL formulae to first order modal -calculus expressions. Our translation takes advantage of the formal treatment of data and parametrized propositional variables in the mCRL2 process and property specifications respectively to address the topology-formulae part of CACTL expressing multi-hop


Model checking, Ad hoc networks, Topology-dependent property, State-space explosion