2013 28th IEEE/ACM International Conference on Automated Software Engineering (ASE), November 11-15, 2013, Palo Alto, USA

Desktop Layout

Technical Research Track
Medtrn. II
Software Model Checking for Distributed Systems with Selector-Based, Non-blocking Communication
Cyrille Artho, Masami Hagiya, Richard Potter, Yoshinori Tanabe, Franz Weitl, and Mitsuharu Yamamoto
(AIST, Japan; University of Tokyo, Japan; National Institute of Informatics, Japan; Chiba University, Japan)
Supplementary Material
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.


Time stamp: 2019-07-23T15:36:07+02:00