Talks & Seminars
Verifying Network Protocol Implementations by Refinement Checking
Rajeev Alur,
Date & Time: August 21, 2002 15:00
Venue: CSE Seminar Hall
Model checking has emerged as a useful verification technique to discover bugs in protocols by comparing finite-state models against logical correctness requirements. We explore its application to the problem of establishing consistency of code implementing a network protocol with respect to the documentation as a standard RFC. The problem is formulated as a refinement checking between two models, the implementation extracted from code and the specification extracted from RFC. After simplifications based on assume-guarantee reasoning, and automatic construction of witness modules to deal with the hidden specification state, the refinement checking problem reduces to checking transition invariants. The methodology is implemented in the model checker MOCHA, and we illustrate it using the case study of PPP (point-to-point protocol for establishing connections remotely).
Speaker Profile:
Rajeev Alur
List of Talks


Faculty CSE IT
Forgot Password
    [+] Sitemap     Feedback