DocumentCode
2004531
Title
Verifying networked programs using a model checker extension
Author
Leungwattanakit, Watcharin ; Artho, Cyrille ; Hagiya, Masami ; Tanabe, Yoshinori ; Yamamoto, Mitsuharu
Author_Institution
Univ. of Tokyo, Tokyo
fYear
2009
fDate
16-24 May 2009
Firstpage
409
Lastpage
410
Abstract
Model checking finds failures in software by exploring every possible execution schedule. Until recently it has been mainly applied to stand-alone applications. This paper presents the I/O-cache, an extension for a Java model checker to support networked programs. It contains a cache module, which captures data streams between a target process and its peer processes. This demonstration also shows how we found a defect in a WebDAV client with a model checker and our extension.
Keywords
Java; cache storage; client-server systems; formal verification; peer-to-peer computing; scheduling; software fault tolerance; I/O-cache; Java model checker; WebDAV client; cache module; data streams; execution schedule; model checker extension; networked programs verification; peer processes; software failures; Application software; Data structures; Dispatching; Java; Libraries; Operating systems; Sockets; Software testing; Web server; Yarn;
fLanguage
English
Publisher
ieee
Conference_Titel
Software Engineering - Companion Volume, 2009. ICSE-Companion 2009. 31st International Conference on
Conference_Location
Vancouver, BC
Print_ISBN
978-1-4244-3495-4
Type
conf
DOI
10.1109/ICSE-COMPANION.2009.5071036
Filename
5071036
Link To Document