loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE '07)
Model Checking Networked Programs in the Presence of Transmission Failures
Shanghai, China
June 06-June 08
ISBN: 0-7695-2856-2
Cyrille Artho, National Institute of Informatics, Tokyo, Japan
Christian Sommer, ETH Z?rich, Zurich, Switzerland
Shinichi Honiden, National Institute of Informatics, Tokyo, Japan
Software model checkers work directly on single-process programs, but not on multiple processes. Conversion of processes into threads, combined with a network model, allows for model checking distributed applications, but does not cover potential communication failures. This paper contributes a fault model for model checking networked programs. If a na?ve fault model is used, spurious deadlocks may appear, because certain processes are terminated before they can complete a necessary action. Such spurious deadlocks have to be suppressed, as implemented in our model checker extension. Our approach found several faults in existing applications, and scales well because exceptions generated by our tool can be checked individually.
Citation:
Cyrille Artho, Christian Sommer, Shinichi Honiden, "Model Checking Networked Programs in the Presence of Transmission Failures," tase, pp.219-228, First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE '07), 2007
Usage of this product signifies your acceptance of the Terms of Use.