Content Dissemination Schemes for Mobile Clouds: Modeling, Analysis, and Verification

Abstract

In this work, we capitalize on our previous work on the Hybrid Scheme for Message Replication (HSM) for opportunistic networks, to develop two content dissemination schemes for mobile clouds, namely, the Forecast and Relay (FAR) and Utility-Based Scheme (UBS). Simulation results with synthetic mobility models validate that the proposed schemes outperform existing routing strategies, such as the PRoPHET, Epidemic, Random, and Wave. We have exploited High-Level Petri Nets to model and analyze the communication processes encompassing HSM, FAR, and UBS. The UBS has been conceived to overcome a crucial design limitation of HSM and FAR, made evident through formal analysis. We have used the New Symbolic Model Verifier (NuSMV) to verify the three schemes against the identified limitation, by using optimization techniques. The verification results affirm the correctness and scalability of the models. The work corroborates that formal verification can be leveraged to design newer and efficient content dissemination schemes.