kirancodes.me
To Proof Maintenance & Beyond!
ASE 2013

Software model checking for distributed systems with selector-based, non-blocking communication

Cyrille Artho, Masami Hagiya, Richard Potter, Yoshinori Tanabe, Franz Weitl, Mitsuharu Yamamoto

Full textDOI 10.1109/ase.2013.6693077dblp

Abstract

Many modern software systems are implemented as client/server architectures, where a server handles multiple clients concurrently. Testing does not cover the outcomes of all possible thread and communication schedules reliably. Software model checking, on the other hand, covers all possible outcomes but is often limited to subsets of commonly used protocols and libraries. Earlier work in cache-based software model checking handles implementations using socket-based TCP/IP networking, with one thread per client connection using blocking input/output. Recently, servers using non-blocking, selector-based input/output have become prevalent. This paper describes our work extending the Java PathFinder extension net-iocache to such software, and the application of our tool to modern server software.

BibTeX
@inproceedings{Artho-al:ASE13,
  author    = {Cyrille Artho and
               Masami Hagiya and
               Richard Potter and
               Yoshinori Tanabe and
               Franz Weitl and
               Mitsuharu Yamamoto},
  title     = {Software model checking for distributed systems with selector-based, non-blocking communication},
  booktitle = {ASE},
  pages     = {169--179},
  publisher = {{IEEE}},
  year      = {2013},
}

Related papers