Network protocol construction is a complex and error prone task. The challenges originate both from the inherent complexity of developing correct program code and from the distributed nature of networked systems. Protocol errors can have devastating consequences. Even so, methods for ensuring protocol correctness are currently only used to a limited extent. A central reason for this is that they are often complex and expensive to employ. In this thesis, we develop methods to perform network protocol testing and verification, with the goal to make the techniques more accessible and readily adoptable.We examine how to formulate correctness requirements for ad hoc routing protocols used to set up forwarding paths in wireless networks. Model checking is a way to verify such requirements automatically. We investigate scalability of finite-state model checking, in terms of network size and topological complexity, and devise a manual abstraction technique to improve scalability.A methodology combining simulations, emulations, and real world experiments is developed for analyzing the performance of wireless protocol implementations. The technique is applied in a comparison of the ad hoc routing protocols AODV, DSR, and OLSR. Discrepancies between simulations and real world behavior are identified; these are due to absence of realistic radio propagation and mobility models in simulation…
Contents
1 Introduction
1.1 Network Protocols
1.2 Protocol Correctness
1.3 Research Issues Addressed in this Thesis
1.3.1 Limiting Code Bugs
1.3.2 Performing Structured Live Testing
1.3.3 Verifying Finite Protocol Instances
1.3.4 Infinite-State Verification
1.4 Contributions
1.4.1 Research Results
1.4.2 Implementation Work
1.4.3 Protocol and Program Models
2 Correct Network Protocol Construction
2.1 Software Development Frameworks
2.2 Modularization
2.3 Program Evaluation
3 Protocol Evaluation Methods
3.1 Protocol Testing
3.1.1 Real-World Testing
3.1.2 Network Simulation
3.1.3 Network Emulation
3.2 Formal Verification
3.2.1 Property Specification
3.2.2 Safety and Liveness Properties .
3.2.3 Model Building
3.2.4 Finite-State Verification
3.2.5 Infinite-State Verification
3.3 Hybrid Evaluation Methods
4 Studied Network Protocols and Their Properties
4.1 Ad Hoc Routing Protocols
4.1.1 LUNAR
4.1.2 DYMO
4.2 Recursive Data Structures
4.3 Ad Hoc Routing Protocol Properties
4.3.1 Performance Properties
4.3.2 Logical Correctness
4.3.3 Heap-Manipulation Properties
5 Developing Correct Ad Hoc Routing Protocols
5.1 Modularizing Code for Different Platforms
5.2 Structured Live Testing
5.3 Model Checking Finite Instances
5.3.1 Properties Studied and Assumptions Imposed
5.3.2 Modeling the Network Medium in SPIN and UPPAAL
5.3.3 Other Modeling Considerations
5.3.4 Verification Results
5.4 Analysis Using Manual Abstraction
5.5 Automatic Infinite-State Verification
5.5.1 Symbolic Backward Analysis
5.5.2 Extension to Heap-Manipulating Programs
5.5.3 Implementation
5.5.4 Verification Results
6 Related Work
7 Conclusions, Impact, and Future Work
A GBT Implementation Details
B GBT Language Reference
C Running GBT
Summary in Swedish
Bibliography
Author: Wibling, Oskar
Source: Uppsala University Library
Download URL 2: Visit Now