Sciweavers

Share
KBSE
2009
IEEE

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

10 years 12 days ago
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
Cyrille Artho, Watcharin Leungwattanakit, Masami H
Added 21 May 2010
Updated 21 May 2010
Type Conference
Year 2009
Where KBSE
Authors Cyrille Artho, Watcharin Leungwattanakit, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto
Comments (0)
books