Finding bugs in network protocols using simulation code and protocol-specific heuristics
In: Formal methods and software engineering (7th international conference on formal engineering methods, ICFEM 2005, Manchester, UK, November 1-4, 2005)0ICFEM 2005 :235-250
Konferenz
- print, 33 ref 1
Zugriff:
Traditional network simulators perform well in evaluating the performance of network protocols but lack the capability of verifying the correctness of protocols. To address this problem, we have extended the J-Sim network simulator with a model checking capability that explores the state space of a network protocol to find an execution that violates a safety invariant. In this paper, we demonstrate the usefulness of this integrated tool for verification and performance evaluation by analyzing two widely used and important network protocols: AODV and directed diffusion. Our analysis discovered a previously unknown bug in the J-Sim implementation of AODV. More importantly, we also discovered a serious deficiency in directed diffusion. To enable the analysis of these fairly complex protocols, we needed to develop protocol-specific search heuristics that guide state-space exploration. We report our findings on discovering good search heuristics to analyze network protocols similar to AODV and directed diffusion.
Titel: |
Finding bugs in network protocols using simulation code and protocol-specific heuristics
|
---|---|
Autor/in / Beteiligte Person: | SOBEIH, Ahmed ; VISWANATHAN, Mahesh ; MARINOV, Darko ; HOU, Jennifer C |
Link: | |
Quelle: | Formal methods and software engineering (7th international conference on formal engineering methods, ICFEM 2005, Manchester, UK, November 1-4, 2005)0ICFEM 2005 :235-250 |
Veröffentlichung: | Berlin: Springer, 2005 |
Medientyp: | Konferenz |
Umfang: | print, 33 ref 1 |
ISSN: | 0302-9743 (print) |
Schlagwort: |
|
Sonstiges: |
|