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

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Graph Grammar Modeling and Verification of Ad Hoc Routing Protocols
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. (Algorithmic Program Verification)
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. (Mobility)
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. (Algorithmic Program Verification)
2008 (English)In: Tools and Algorithms for the Construction and Analysis of Systems, Berlin: Springer-Verlag , 2008, 18-32 p.Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Berlin: Springer-Verlag , 2008. 18-32 p.
Series
Lecture Notes in Computer Science, 4963
National Category
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-96981DOI: 10.1007/978-3-540-78800-3_3ISI: 000254735100003OAI: oai:DiVA.org:uu-96981DiVA: diva2:171736
Available from: 2008-03-28 Created: 2008-03-28 Last updated: 2011-02-27Bibliographically approved
In thesis
1. Verifying Absence of ∞ Loops in Parameterized Protocols
Open this publication in new window or tab >>Verifying Absence of ∞ Loops in Parameterized Protocols
2008 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

The complex behavior of computer systems offers many challenges for formal verification. The analysis quickly becomes difficult as the number of participating processes increases.

A parameterized system is a family of systems parameterized on a number n, typically representing the number of participating processes. The uniform verification problem — to check whether a property holds for each instance — is an infinite-state problem. The automated analysis of parameterized and infinite-state systems has been the subject of research over the last 15–20 years. Much of the work has focused on safety properties. Progress in verification of liveness properties has been slow, as it is more difficult in general.

In this thesis, we consider verification of parameterized and infinite-state systems, with an emphasis on liveness, in the verification framework called regular model checking (RMC). In RMC, states are represented as words, sets of states as regular expressions, and the transition relation as a regular relation.

We extend the automata-theoretic approach to RMC. We define a specification logic sufficiently strong to specify systems representable using RMC, and linear temporal logic properties of such systems, and provide an automatic translation from a specification into an analyzable model.

We develop acceleration techniques for RMC which allow more uniform and automatic verification than before, with greater power. Using these techniques, we succeed to verify safety and liveness properties of parameterized protocols from the literature.

We present a novel reachability based verification method for verification of liveness, in a general setting. We implement the method for RMC, with promising results.

Finally, we develop a framework for the verification of dynamic networks based on graph transformation, which generalizes the systems representable in RMC. In this framework we verify the latest version of the DYMO routing protocol, currently being considered for standardization by the IETF.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis, 2008. 80 p.
Series
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 419
Keyword
formal methods, verification, model checking, infinite-state systems, regular model checking, liveness, graph transformation
Identifiers
urn:nbn:se:uu:diva-8605 (URN)978-91-554-7148-4 (ISBN)
Public defence
2008-04-18, 2446, MIC, Polacksbacken, Uppsala, 13:15
Opponent
Supervisors
Available from: 2008-03-28 Created: 2008-03-28 Last updated: 2011-02-18Bibliographically approved
2. 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.
Series
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 571
Keyword
network protocols, formal methods, verification, testing, routing protocols, wireless ad hoc networks, model checking, graph transformation, infinite-state systems
National Category
Computer Science
Identifiers
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)
Opponent
Supervisors
Available from: 2008-11-13 Created: 2008-11-13 Last updated: 2011-02-18Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Authority records BETA

Saksena, MayankWibling, OskarJonsson, Bengt

Search in DiVA

By author/editor
Saksena, MayankWibling, OskarJonsson, Bengt
By organisation
Computer Systems
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 662 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf