Cache-Based Model Checking of Networked Applications: From Linear to Branching Time

Abstract—Many applications are concurrent and communicate over a network. The non-determinism in the thread and communication schedules makes it desirable to model check such systems. However, a simple state space exploration scheme is not applicable, as backtracking results in repeated communication operations. A cache-based approach solves this problem by hiding redundant communication operations from the environment. In this work, we propose a change from a linear-time to a branching-time cache, allowing us to relax restrictions in previous work regarding communication traces that differ between schedules. We successfully applied the new algorithm to real-life programs where a previous solution is not applicable. Keywords-Software model checking; software verification; networking; input/output; caching

• Type: Conference
• Year: 2009
• Where: KBSE
• Authors: Cyrille Artho, Watcharin Leungwattanakit, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto
• Keywords: Communication Operations, KBSE 2009, Redundant Communication Operations, Repeated Communication Operations, Software Engineering