{"id":{"repo_id":"buffalo","oai_identifier":"oai:ubir.buffalo.edu:10477/77949"},"canonical_url":"https://search.dev.ndltd.org/etd/buffalo/oai:ubir.buffalo.edu:10477/77949","repository":{"repo_id":"buffalo","name":"Buffalo","base_url":"https://ubir.buffalo.edu/oai/request"},"display":{"title":"Model-Based Runtime Verification Framework for Wireless Protocol Implementations","abstract":"Ph.D.","abstract_html":"Ph.D.","abstract_has_math":false,"creators":["Shi, Jinghao; 0000-0002-6516-9865"],"institution":"State University of New York at Buffalo","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":["Challen, Geoffrey","Computer Science and Engineering"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2018,"date_issued":"2018-06-28T20:31:41Z","date_published":"2018-06-28T20:31:41Z","updated_at":"2026-07-27T19:05:05Z","subjects":["computer science"],"languages":["eng"],"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."],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/10477/77949","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Challen, Geoffrey","Computer Science and Engineering"]},{"key":"dc:creator","label":"Author","values":["Shi, Jinghao; 0000-0002-6516-9865"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2018-06-28T20:31:41Z","2018","2018-02-02 15:20:22"]},{"key":"dc:publisher","label":"Institution","values":["State University of New York at Buffalo"]},{"key":"dc:type","label":"Dc Type","values":["Text","Dissertation"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["computer science"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["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."]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/10477/77949"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Ph.D.","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."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Model-Based Runtime Verification Framework for Wireless Protocol Implementations"]}]}],"canonical_facts":{"dc:contributor":["Challen, Geoffrey","Computer Science and Engineering"],"dc:creator":["Shi, Jinghao; 0000-0002-6516-9865"],"dc:date":["2018-06-28T20:31:41Z","2018","2018-02-02 15:20:22"],"dc:description":["Ph.D.","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."],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/10477/77949"],"dc:language":["eng"],"dc:publisher":["State University of New York at Buffalo"],"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."],"dc:subject":["computer science"],"dc:title":["Model-Based Runtime Verification Framework for Wireless Protocol Implementations"],"dc:type":["Text","Dissertation"]},"updated_at":"2026-07-27T19:05:05Z"}