uu.seUppsala University Publications
Change search
ReferencesLink to record
Permanent link

Direct link
Symbolic Backward Reachability with Summary Nodes for Graph Grammar Verification
Uppsala University, Teknisk-naturvetenskapliga vetenskapsområdet, Mathematics and Computer Science, Department of Information Technology.
Article in journal (Refereed) Submitted
URN: urn:nbn:se:uu:diva-97749OAI: oai:DiVA.org:uu-97749DiVA: diva2:172803
Available from: 2008-11-13 Created: 2008-11-13Bibliographically approved
In thesis
1. Creating Correct Network Protocols
Open this publication in new window or tab >>Creating Correct Network Protocols
2008 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

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. The issues are mainly related to how the protocols sense their network surroundings and we identify improvements to these capabilities.

Finally, we develop a methodology and a tool for automatic verification of safety properties of infinite-state network protocols, modeled as graph transformation systems extended with negative application conditions. The verification uses symbolic backward reachability analysis. By introducing abstractions in the form of summary nodes, the method is extended to protocols with recursive data structures. Our tool automatically verifies correct routing of the DYMO ad hoc routing protocol and several nontrivial heap manipulating programs.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis, 2008. 118 p.
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 571
network protocols, formal methods, verification, testing, routing protocols, wireless ad hoc networks, model checking, graph transformation, infinite-state systems
National Category
Computer Science
urn:nbn:se:uu:diva-9361 (URN)978-91-554-7333-4 (ISBN)
Public defence
2008-12-05, Häggsalen, Ångströmlaboratoriet, Lägerhyddsvägen 1, Uppsala, 14:15 (English)
Available from: 2008-11-13 Created: 2008-11-13 Last updated: 2011-02-18Bibliographically approved

Open Access in DiVA

No full text

By organisation
Department of Information Technology

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 188 hits
ReferencesLink to record
Permanent link

Direct link