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 -