Analysis and implementation of formal models for Sensor and Mobile Ad Hoc Networks

Connectivity, Interference and Energy conservations, are key aspects in Mobile Ad Hoc Networks (MANETS). I propose a Probabilistic Energy -aware calculus for the analysis of both such aspects of MANETS. This calculus is a probabilistic process algebra, in the style of CCS, capturing essential characteristics of Mobile Ad Hoc Networks, including the ability of nodes to broadcast a message to any other node within its physical transmission range, and to move in and out of the transmission range of other nodes in the network. Probability distributions are used to described the mobility of nodes. The semantic is inspired to Segala’s probabilistic automata, driven by schedulers to resolve the non-deterministic choices among the probability distributions over target states. A probabilistic observational congruence has been defined together with a bisimulation-based proof technique. Finally two different preorders has been defined in order to verify whether two networks exhibit the same observable probabilistic behavior in terms of connectivity, but with dfferent performances in terms of energy conservation or Interference.