Model-Based Runtime Verification Framework for Wireless Protocol Implementations

Validating wireless protocol implementations is challenging. Today's approaches re­ quire labor-intensive experimental setup and manual trace investigation, but produce poor coverage and inaccurate and irreproducible results. We present VERIFI, the first systematic sniffer-based, model-guided runtime verification framework for wireless pro­ tocol implementations. VERIFI takes a formal model of the protocol being verified as input. To achieve good coverage, it first applies state reachability analysis by ap­ plying model checking techniques. It then uses a new PACKETSNIPER component to selectively trigger packet losses required to quickly investigate all reachable protocol states. Our results show that the selective packet jamming allows VERIFI to signif­ icantly improve the coverage of protocol states. Finally, VERIFI accommodates un­ certainty caused by the sniffer when validating traces, allowing it to provide accurate and reproducible results. By modeling uncertainty, VERIFI highlights likely protocol violations for developers to examine.

Grantor dc:publisher

State University of New York at Buffalo

Year dc:date.issued

2018

Author dc:creator

• Shi, Jinghao; 0000-0002-6516-9865

Contributors dc:contributor

• Challen, Geoffrey
• Computer Science and Engineering

• computer science

Statement dc:rights

• Users of works found in University at Buffalo Institutional Repository (UBIR) are responsible for identifying and contacting the copyright owner for permission to reuse. University at Buffalo Libraries do not manage rights for copyright-protected works and cannot assist with permissions.
• Copyright retained by author.

Language dc:language

eng

Handle dc:identifier

http://hdl.handle.net/10477/77949

OAI record oai:identifier

https://ubir.buffalo.edu/oai/request?verb=GetRecord&metadataPrefix=qdc&identifier=oai%3Aubir.buffalo.edu%3A10477%2F77949