Model Checking Networked Programs in the Presence of Transmission Failures

Cyrille Artho, Christian Sommer, and Shinichi Honiden

Semester thesis of Christian Sommer, paper presented at TASE 2007 (Theoretical Aspects of Software Engineering) in Shanghai

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.

• Model Checking Networked Programs in the Presence of Transmission Failures, paper
• preprint
• addioexc.zip 140 KB, code, includes JPFSearch class and code instrumentation, requires SERP (included in zip)
• Java PathFinder

@inproceedings{ash07,
  author = {Cyrille Artho and Christian Sommer and Shinichi Honiden},
  title = {Model Checking Networked Programs in the Presence of Transmission Failures},
  booktitle = {Proc.\ 1st Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE~2007)},
  pages = {219--228},
  year = {2007},
}