Model checking networked programs in the presence of transmission failures

Cyrille Artho, Christian Sommer, Shinichi Honiden

Research output: Chapter in Book/Report/Conference proceedingConference contribution

10 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationFirst Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE '07
Pages219-228
Number of pages10
DOIs
Publication statusPublished - 2007 Sep 27
Event1st Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE '07 - Shanghai, China
Duration: 2007 Jun 62007 Jun 8

Publication series

NameFirst Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE '07

Other

Other1st Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE '07
CountryChina
CityShanghai
Period07/6/607/6/8

    Fingerprint

ASJC Scopus subject areas

  • Computer Science(all)

Cite this

Artho, C., Sommer, C., & Honiden, S. (2007). Model checking networked programs in the presence of transmission failures. In First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE '07 (pp. 219-228). [4239966] (First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE '07). https://doi.org/10.1109/TASE.2007.33