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
Externally publishedYes
Event1st Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE '07 - Shanghai, China
Duration: 2007 Jun 62007 Jun 8

Other

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

Fingerprint

Model checking
Communication

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] https://doi.org/10.1109/TASE.2007.33

Model checking networked programs in the presence of transmission failures. / Artho, Cyrille; Sommer, Christian; Honiden, Shinichi.

First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE '07. 2007. p. 219-228 4239966.

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

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., 4239966, pp. 219-228, 1st Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE '07, Shanghai, China, 07/6/6. https://doi.org/10.1109/TASE.2007.33
Artho C, Sommer C, Honiden S. Model checking networked programs in the presence of transmission failures. In First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE '07. 2007. p. 219-228. 4239966 https://doi.org/10.1109/TASE.2007.33
Artho, Cyrille ; Sommer, Christian ; Honiden, Shinichi. / Model checking networked programs in the presence of transmission failures. First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE '07. 2007. pp. 219-228
@inproceedings{d97657ef0c3d4bdeaa3e898880474b51,
title = "Model checking networked programs in the presence of transmission failures",
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{\"i}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.",
author = "Cyrille Artho and Christian Sommer and Shinichi Honiden",
year = "2007",
month = "9",
day = "27",
doi = "10.1109/TASE.2007.33",
language = "English",
isbn = "0769528562",
pages = "219--228",
booktitle = "First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE '07",

}

TY - GEN

T1 - Model checking networked programs in the presence of transmission failures

AU - Artho, Cyrille

AU - Sommer, Christian

AU - Honiden, Shinichi

PY - 2007/9/27

Y1 - 2007/9/27

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=34548817557&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=34548817557&partnerID=8YFLogxK

U2 - 10.1109/TASE.2007.33

DO - 10.1109/TASE.2007.33

M3 - Conference contribution

AN - SCOPUS:34548817557

SN - 0769528562

SN - 9780769528564

SP - 219

EP - 228

BT - First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE '07

ER -