EfficientModelCheckingofApplicationswithInputOutput-.PDFVIP

E?cient Model Checking of Applications with Input/Output Cyrille Artho1, Boris Zweimuller¨ 2, Armin Biere3, Etsuya Shibayama1, and Shinichi Honiden4 1 Research Center for Information Security (RCIS), National Inst. of Advanced Industrial Science and Technology (AIST), Tokyo, Japan 2 Computer Systems Institute, ETH Zurich,¨ Switzerland 3 Johannes Kepler University, Linz, Austria 4 National Institute of Informatics, Tokyo, Japan 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 re- visiting 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: Software model checking, network communication, software testing 1 Introduction Model checking explores the entire behavior of a system under test (SUT) by investigating each reachable system state [5] for di?erent thread schedules. Re- cently, model checking has been applied directly to software [2,4,6,7,13]. However, conventional software model checking techniques are not applicable to networked programs. The problem is that state space exploration involves backtracking. After backtracking, the model checker will execute certain parts of the program (and thus certain input/output operations) again. However, external processes, which are not under the control of the model checking engine, cannot be kept in synchronization with backtracking, causing direct communication between the SUT and external processes to fail. Our work proposes a solution to this problem. It covers all