HOL/SPIN

Routing information protocol in HOL/SPIN We provide a proof using HOL and SPIN of convergence for the Routing Information Protocol (RIP), an internet protocol based on distance vector routing. We also calculate a sharp realtime bound for this convergence. This extends existing results to deal with the RIP standard itself, which has complexities not accounted for in theorems about abstract versions of the protocol. Our work also provides a case study in the combined use of a higher-order theorem prover and a model checker. The former is used to express abstraction properties and inductions, and structure the high-level proof, while the latter deals efficiently with case analysis of finitary properties


References in zbMATH (referenced in 24 articles , 1 standard article )

Showing results 1 to 20 of 24.
Sorted by year (citations)

1 2 next

  1. Yousefi, Behnaz; Ghassemi, Fatemeh; Khosravi, Ramtin: Modeling and efficient verification of wireless ad hoc networks (2017)
  2. Bres, Emile; van Glabbeek, Rob; Höfner, Peter: A timed process algebra for wireless networks with an application in routing (extended abstract) (2016)
  3. Feo-Arenis, Sergio; Westphal, Bernd; Dietsch, Daniel; Muñiz, Marco; Andisha, Siyar; Podelski, Andreas: Ready for testing: ensuring conformance to industrial standards through formal verification (2016) ioport
  4. Ghassemi, Fatemeh; Fokkink, Wan: Model checking mobile ad hoc networks (2016)
  5. Liu, Si; Ölveczky, Peter Csaba; Meseguer, José: Modeling and analyzing mobile ad hoc networks in Real-Time Maude (2016)
  6. van Glabbeek, Rob; Höfner, Peter; Portmann, Marius; Tan, Wee Lum: Modelling and verifying the AODV routing protocol (2016)
  7. Chen, Chen; Jia, Limin; Xu, Hao; Luo, Cheng; Zhou, Wenchao; Loo, Boon Thau: A program logic for verifying secure routing protocols (2015)
  8. Merro, Massimo; Sibilio, Eleonora: A calculus of trustworthy ad hoc networks (2013)
  9. Fehnker, Ansgar; van Glabbeek, Rob; Höfner, Peter; McIver, Annabelle; Portmann, Marius; Tan, Wee Lum: A process algebra for wireless mesh networks (2012)
  10. Ghassemi, Fatemeh; Fokkink, Wan; Movaghar, Ali: Verification of mobile ad hoc networks: an algebraic approach (2011)
  11. Nanz, Sebastian; Nielson, Flemming; Nielson, Hanne Riis: Static analysis of topology-dependent broadcast networks (2010)
  12. Pura, Mihai-Lica; Patriciu, Victor-Valeriu; Bica, Ion: Formal verification of secure ad hoc routing protocols using AVISPA: ARAN case study (2010)
  13. Singh, Anu; Ramakrishnan, C.R.; Smolka, Scott A.: A process calculus for mobile ad hoc networks (2010)
  14. Billington, Jonathan; Yuan, Cong: On modelling and analysing the dynamic MANET on-demand (DYMO) routing protocol (2009) ioport
  15. Hoang, Thai Son; Kuruma, Hironobu; Basin, David; Abrial, Jean-Raymond: Developing topology discovery in Event-B (2009)
  16. Hoang, Thai Son; Kuruma, Hironobu; Basin, David; Abrial, Jean-Raymond: Developing topology discovery in Event-B (2009)
  17. Espensen, Kristian L.; Kjeldsen, Mads K.; Kristensen, Lars M.: Modelling and initial validation of the DYMO routing protocol for mobile ad-hoc networks (2008)
  18. Ghassemi, Fatemeh; Movaghar, Ali: Modeling routing protocols in adhoc networks (2008)
  19. Saksena, Mayank; Wibling, Oskar; Jonsson, Bengt: Graph grammar modeling and verification of ad hoc routing protocols (2008)
  20. Nanz, Sebastian; Hankin, Chris: A framework for security analysis of mobile wireless networks (2006)

1 2 next