Navigation
Home > Teaching > Analysis and Verification of Network Protocols

Seminar Analysis and Verification of Network Protocols

Winter term 2008/2009

Dr. rer. nat. Thomas Haenselmann,
Peter Backes

Important Dates

  • July 2, 2008 (Wednesday) 14:00 ct.: Kickoff meeting in room 401, building E1 3
  • October 28, 2008 (Tuesday) 14:00 ct.: Second meeting in room 401, building E1 3.

News

General Information

We are going to discuss methods for model checking of communication protocols and autonomous agents. The emphasis will be on two major problems in this field: How to avoid the combinatorial explosion of states and how to handle communication that involves an unbounded number of processes (ad hoc networks, for example).

You will especially benefit from the seminar if you combine it with the practical core lecture Data Networks and/or with the theoretical core lecture Verification, but it's not a prerequisite that you have already attended them or are attending them in parallel.

Requirements

To pass this seminar, you have to

  • give a presentation (English), based on a research paper (40 to 45 minutes).
  • write a seminar paper (English or German) about your topic (ca 15 pages).
  • hand in
    • an outline of your talk two weeks before,
    • an advanced draft of your talk one week before,
    • a substantial draft of your paper three weeks after it,
    • the final version of your paper until March 5
    The first three of these requirements are to be seen as a basis for feedback and criticism. They will not be a basis for grading, only your actual talk and the final version of your paper will be taken into account for that. Hence, you do not need to polish your outline and your drafts and you do not need to submit them by email, either. Instead, please bring them with you on your laptop, on an USB stick or on your scratchpad, show them to Peter Backes in his office and discuss possible improvements.

Schedule

Please note that most of the papers have been linked to their official online copy. You can access the fulltext only from machines that have a campus network IP and so benefit from the Nationallizenz. Machines on the campus network should be fine, including the student PCs of the CIP pool. If you are using your laptop on the university WLAN, it should work, too. You may or may not be lucky to find freely available preprints using a search engine. Please send an email if you still have problems accessing the papers.

Topic Speaker Date
Protocol verification made simple: a tutorial Julian BackesNovember 5
On Communicating Finite-State MachinesJanosch OffenbergNovember 12
Formal Verification of Web Applications Modeled by Communicating AutomataHong Anh LeNovember 19
Inductive Verification and Validation of the KULRoT RoboCup Team Stephanie EhrbächerNovember 26
Symbolic Protocol Verification with Queue BDDsHina ManzurDecember 3
The Power of QDDsDavid SpielerDecember 3
Automatized Verification of Ad Hoc Routing ProtocolsYves NeisiusDecember 10
The Model Checker SPINWenkai DaiDecember 10
Automatic verification of finite-state concurrent systems using temporal logic specificationsAliaksandr TalaikaDecember 17
Verifying Network Protocol Implementations by Symbolic Refinement CheckingBahjat SalibaJanuary 7
Model Checking Agent DialoguesFatemeh ShiraziJanuary 21
Model Checking Linear Properties of Prefix-Recognizable SystemsKaloyan RusevJanuary 28
Symmetry and Reduced Symmetry in Model CheckingPatrick DubbertFebruary 4
Verification of Infinite-State Systems by Combining Abstraction and Reachability AnalysisHanna MousaFebruary 11
A Practical Approach to Coverage in Model CheckingMarc PätzoldMarch 2

Literature

  • Gerard J. Holzmann: Design and validation of computer protocols (Upper Saddle River, NJ: Prentice-Hall, Inc., 1991), ISBN 0-13-539925-4
  • Richard Lai, Ajin Jirachiefpattana: Communication Protocol Specification and Verification (Boston: Kluwer Academic Publishers, 1998)
  • C. A. Sunshine: Communication protocol modeling (Dedham, Mass: Artech House, 1981), ISBN 0890060975
  • Kenneth L. McMillan: Symbolic Model Checking (1993), ISBN 0792393805
  • Robert P. Kurshan: Computer Aided Verification of Coordinating Processes (Princeton Univ. Press, 1995), ISBN 0691034362
  • Behcet Sarikaya: Principles of Protocol Engineering and Conformance Testing (Ellis Horwood, 1993), ISBN 013012642X
  • Hartmut König: Protocol Engineering: Prinzip, Beschreibung und Entwicklung von Kommunikationsprodokollen (Vieweg+Teubner, 2003), ISBN 3519004542