Hiding Backtracking Operations in Software Model Checking from the Environment
Cyrille Valentin Artho, Watcharin Leungwattanakit, Masami Hagiya, Yoshinori Tanabe, Etsuya Shibayama · 2007
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: Backtracking during the state space search causes states to be revisited, and I/O operations to be repeated. Because I/O operations are visible by the environment, software model checking needs to encapsulate such operations in a caching layer that hides such actions. In order to mediate between the model checker and the environment, the cache layer has to pair request and response messages correctly. It also has to distinguish between complete and partial messages. Finally, operations that open or close communication channels require special treatment as well. — Software model checkers [3] cannot handle networked programs, which limits their applicability. Program transformations allow networked applications to be model checked on a single-process model checker [1]. However, the large number of thread interleavings limits scalability. A different approach consists of mediating between backtracking state space exploration of the model checker, and the linear time line of its environment [2]. This approach caches any operations that have an externally visible impact, in particular, network communication. Previous work has assigned a mapping of each communication state to a previously seen communication trace. Each operation is mapped to a history of known operations, extending that history (“cache”) if new states are explored. Whenever a mismatch between states is encountered after backtracking, network communication inside the program depends on its thread schedule. Such programs cannot be verified with our approach; they are also often faulty.