kirancodes.me
To Proof Maintenance & Beyond!
ASE 2009

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

Cyrille Artho, Watcharin Leungwattanakit, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto

Full textDOI 10.1109/ase.2009.43dblp

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.

BibTeX
@inproceedings{Artho-al:ASE09,
  author    = {Cyrille Artho and
               Watcharin Leungwattanakit and
               Masami Hagiya and
               Yoshinori Tanabe and
               Mitsuharu Yamamoto},
  title     = {{Cache-Based} Model Checking of Networked Applications: From Linear to Branching Time},
  booktitle = {ASE},
  pages     = {447--458},
  publisher = {{IEEE} Computer Society},
  year      = {2009},
}

Related papers