Efficient model checking of applications with input/output

Cyrille Artho; Boris Zweimüller; Armin Bière; Etsuya Shibayama; Shinichi Honiden

doi:10.1007/978-3-540-75867-9_65

Efficient model checking of applications with input/output

Cyrille Artho^*, Boris Zweimüller, Armin Bière, Etsuya Shibayama, Shinichi Honiden

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

3 Citations (Scopus)

Abstract

Most non-trivial applications use some form of input/output (I/O), such as network communication. When model checking such an application, a simple state space exploration scheme is not applicable, as the process being model checked would replay I/O operations when revisiting a given state. Thus software model checking needs to encapsulate such operations in a caching layer that is capable of hiding redundant executions of I/O operations from the environment.

Original language	English
Title of host publication	Computer Aided Systems Theory - EUROCAST 2007 - 11th International Conference on Computer Aided Systems Theory, Revised Selected Papers
Publisher	Springer Verlag
Pages	515-522
Number of pages	8
ISBN (Print)	9783540758662
DOIs	https://doi.org/10.1007/978-3-540-75867-9_65
Publication status	Published - 2007
Externally published	Yes
Event	11th International Conference on Computer Aided Systems Theory, EUROCAST 2007 - Las Palmas de Gran Canaria, Spain Duration: 2007 Feb 12 → 2007 Feb 16

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	4739 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	11th International Conference on Computer Aided Systems Theory, EUROCAST 2007
Country/Territory	Spain
City	Las Palmas de Gran Canaria
Period	07/2/12 → 07/2/16

Keywords

Network communication
Software model checking
Software testing

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-540-75867-9_65

Cite this

Artho, C., Zweimüller, B., Bière, A., Shibayama, E., & Honiden, S. (2007). Efficient model checking of applications with input/output. In Computer Aided Systems Theory - EUROCAST 2007 - 11th International Conference on Computer Aided Systems Theory, Revised Selected Papers (pp. 515-522). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4739 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-540-75867-9_65

Efficient model checking of applications with input/output. / Artho, Cyrille; Zweimüller, Boris; Bière, Armin et al.

Computer Aided Systems Theory - EUROCAST 2007 - 11th International Conference on Computer Aided Systems Theory, Revised Selected Papers. Springer Verlag, 2007. p. 515-522 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4739 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Artho, C, Zweimüller, B, Bière, A, Shibayama, E & Honiden, S 2007, Efficient model checking of applications with input/output. in Computer Aided Systems Theory - EUROCAST 2007 - 11th International Conference on Computer Aided Systems Theory, Revised Selected Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4739 LNCS, Springer Verlag, pp. 515-522, 11th International Conference on Computer Aided Systems Theory, EUROCAST 2007, Las Palmas de Gran Canaria, Spain, 07/2/12. https://doi.org/10.1007/978-3-540-75867-9_65

Artho C, Zweimüller B, Bière A, Shibayama E, Honiden S. Efficient model checking of applications with input/output. In Computer Aided Systems Theory - EUROCAST 2007 - 11th International Conference on Computer Aided Systems Theory, Revised Selected Papers. Springer Verlag. 2007. p. 515-522. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-540-75867-9_65

Artho, Cyrille ; Zweimüller, Boris ; Bière, Armin et al. / Efficient model checking of applications with input/output. Computer Aided Systems Theory - EUROCAST 2007 - 11th International Conference on Computer Aided Systems Theory, Revised Selected Papers. Springer Verlag, 2007. pp. 515-522 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{965f73cf2b3f44d6bf35fd24df487019,

title = "Efficient model checking of applications with input/output",

abstract = "Most non-trivial applications use some form of input/output (I/O), such as network communication. When model checking such an application, a simple state space exploration scheme is not applicable, as the process being model checked would replay I/O operations when revisiting a given state. Thus software model checking needs to encapsulate such operations in a caching layer that is capable of hiding redundant executions of I/O operations from the environment.",

keywords = "Network communication, Software model checking, Software testing",

author = "Cyrille Artho and Boris Zweim{\"u}ller and Armin Bi{\`e}re and Etsuya Shibayama and Shinichi Honiden",

year = "2007",

doi = "10.1007/978-3-540-75867-9_65",

language = "English",

isbn = "9783540758662",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "515--522",

booktitle = "Computer Aided Systems Theory - EUROCAST 2007 - 11th International Conference on Computer Aided Systems Theory, Revised Selected Papers",

note = "11th International Conference on Computer Aided Systems Theory, EUROCAST 2007 ; Conference date: 12-02-2007 Through 16-02-2007",

}

TY - GEN

T1 - Efficient model checking of applications with input/output

AU - Artho, Cyrille

AU - Zweimüller, Boris

AU - Bière, Armin

AU - Shibayama, Etsuya

AU - Honiden, Shinichi

PY - 2007

Y1 - 2007

N2 - Most non-trivial applications use some form of input/output (I/O), such as network communication. When model checking such an application, a simple state space exploration scheme is not applicable, as the process being model checked would replay I/O operations when revisiting a given state. Thus software model checking needs to encapsulate such operations in a caching layer that is capable of hiding redundant executions of I/O operations from the environment.

AB - Most non-trivial applications use some form of input/output (I/O), such as network communication. When model checking such an application, a simple state space exploration scheme is not applicable, as the process being model checked would replay I/O operations when revisiting a given state. Thus software model checking needs to encapsulate such operations in a caching layer that is capable of hiding redundant executions of I/O operations from the environment.

KW - Network communication

KW - Software model checking

KW - Software testing

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

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

U2 - 10.1007/978-3-540-75867-9_65

DO - 10.1007/978-3-540-75867-9_65

M3 - Conference contribution

AN - SCOPUS:38449092931

SN - 9783540758662

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 515

EP - 522

BT - Computer Aided Systems Theory - EUROCAST 2007 - 11th International Conference on Computer Aided Systems Theory, Revised Selected Papers

PB - Springer Verlag

T2 - 11th International Conference on Computer Aided Systems Theory, EUROCAST 2007

Y2 - 12 February 2007 through 16 February 2007

ER -

Efficient model checking of applications with input/output

Abstract

Publication series

Other

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this