Abstract
Due to the highly dynamic behavior and the time complexity in Mobile Ad-hoc NEtworks (MANETs), modeling distributed algorithms and looking at their assumptions represent a challenging research task. Also, proving the correctness of these algorithms for dynamic networks is a topic of intensive research. In fact, the solutions which have been proposed to express and prove the correctness of distributed algorithms are usually done manually. In addition, all these solutions lack a consensus about their development and their proof. The main contribution of this paper is to propose a general and formal model for dynamic networks based on evolving graphs and Event-B formal method. In fact, evolving graphs is a powerful tool to express fine-grained properties. This model allows to handle topological events and to characterize the concept of time with some particularities. We implement it with Event-B, based on refinement technique. To illustrate the proposed model, we investigate an example of a distributed algorithm encoded by local computations models.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Abrial, J.: Modeling in Event-B–System and Software Engineering. Cambridge University Press, Cambridge (2010)
Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in event-b. Int. J. Softw. Tools Technol. Transf. 12(6), 447–466 (2010)
Back, R.J.R.: A calculus of refinements for program derivations. Acta Informatica 25, 593–624 (1988)
Barjon, M., Casteigts, A., Chaumette, S., Johnen, C., Neggaz, Y.M.: Maintaining a spanning forest in highly dynamic networks: the synchronous case. In: Proceedings of the Principles of Distributed Systems–18th International Conference, OPODIS 2014, Cortina d’Ampezzo, Italy, 16-19 December 2014, pp. 277-292 (2014)
Bui-Xuan, B.M., Ferreira, A., Jarry, A.: Computing shortest, fastest, and foremost journeys in dynamic networks. Int. J. Found. Comput. Sci. 14, 267–285 (2003)
Casteigts, A.: Contribution à l’algorithmique distribué dans les réseaux mobiles ad hoc. Ph.D. thesis, Université Sciences et Technologies–Bordeaux I (2007)
Casteigts, A., Chaumette, S., Ferreira, A.: Distributed Computing in Dynamic Networks: Towards a Framework for Automated Analysis of Algorithms. CoRR, abs/1102.5529 (2012)
Ferreira, A.: Building a reference combinatorial model for MANETs. IEEE Network 18(5), 24–29 (2004)
Floriano, P., Goldman, A., Arantes, L.: Formalization of the necessary and sufficient connectivity conditions to the distributed mutual exclusion problem in dynamic networks. In: Proceedings of the 2011 IEEE 10th International Symposium on Network Computing and Applications, NCA’11, pp. 203-210. IEEE Computer Society, Washington (2011)
Kerchove, F.M.D.: Relabeling Algorithms on Dynamic Graphs. Technical report, University of Le Havre (2012)
Leavens, G.T., Abrial, J.R., Batory, D., Butler, M., Coglio, A., Fisler, K., Hehner, E., Jones, C., Miller, D., Peyton-Jones, S., Sitaraman, M., Smith, D.R., Stump, A.: Roadmap for enhanced languages and methods to aid verification. In: Proceedings of the 5th International Conference on Generative Programming and Component Engineering, GPCE’06, pp. 221-236. ACM, New York (2006)
Litovsky, I., Métivier, Y., Sopena, E.: Handbook of graph grammars and computing by graph transformation. In: Graph Relabelling Systems and Distributed Algorithms, pp. 1-56. World Scientific Publishing Co., Inc., River Edge (1999)
Roy, R.: Mobile ad hoc networks. In: Handbook of Mobile Ad Hoc Networks for Mobility Models, pp. 3-22. Springer, New York (2011)
Tel, G.: Introduction to Distributed Algorithms, 2nd edn. Cambridge University Press, New York (2001)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Fakhfakh, F., Tounsi, M., Kacem, A.H., Mosbah, M. (2016). Towards a Formal Model for Dynamic Networks Through Refinement and Evolving Graphs. In: Lee, R. (eds) Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computing 2015. Studies in Computational Intelligence, vol 612. Springer, Cham. https://doi.org/10.1007/978-3-319-23509-7_16
Download citation
DOI: https://doi.org/10.1007/978-3-319-23509-7_16
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-23508-0
Online ISBN: 978-3-319-23509-7
eBook Packages: EngineeringEngineering (R0)