Title :
Modular Software Model Checking for Distributed Systems
Author :
Leungwattanakit, Watcharin ; Artho, Cyrille ; Hagiya, Masami ; Tanabe, Y. ; Yamamoto, Manabu ; Takahashi, Koichi
Author_Institution :
Dept. of Math. & Inf., Chiba Univ., Chiba, Japan
Abstract :
Distributed systems are complex, being usually composed of several subsystems running in parallel. Concurrent execution and inter-process communication in these systems are prone to errors that are difficult to detect by traditional testing, which does not cover every possible program execution. Unlike testing, model checking can detect such faults in a concurrent system by exploring every possible state of the system. However, most model-checking techniques require that a system be described in a modeling language. Although this simplifies verification, faults may be introduced in the implementation. Recently, some model checkers verify program code at runtime but tend to be limited to stand-alone programs. This paper proposes cache-based model checking, which relaxes this limitation to some extent by verifying one process at a time and running other processes in another execution environment. This approach has been implemented as an extension of Java PathFinder, a Java model checker. It is a scalable and promising technique to handle distributed systems. To support a larger class of distributed systems, a checkpointing tool is also integrated into the verification system. Experimental results on various distributed systems show the capability and scalability of cache-based model checking.
Keywords :
Java; cache storage; checkpointing; concurrency control; distributed processing; program testing; program verification; Java PathFinder extension; Java model checker; cache-based model checking; checkpointing tool; concurrent execution; distributed systems; execution environment; fault detection; interprocess communication; model-checking techniques; modeling language; modular software model checking; parallel subsystems; program code verification; program execution; stand-alone programs; Checkpointing; Java; Message systems; Model checking; Scalability; Software; Synchronization; Software model checking; checkpointing; distributed systems; software verification;
Journal_Title :
Software Engineering, IEEE Transactions on
DOI :
10.1109/TSE.2013.49