Home

Distributed eXplode: A High-Performance Model Checking Engine to Scale Up State-Space Coverage

Nageswar Keetha; Leon Li Wu; Gail E. Kaiser; Junfeng Yang

Title:
Distributed eXplode: A High-Performance Model Checking Engine to Scale Up State-Space Coverage
Author(s):
Keetha, Nageswar
Wu, Leon Li
Kaiser, Gail E.
Yang, Junfeng
Date:
Type:
Technical reports
Department:
Computer Science
Permanent URL:
Series:
Columbia University Computer Science Technical Reports
Part Number:
CUCS-051-08
Publisher:
Department of Computer Science, Columbia University
Publisher Location:
New York
Abstract:
Model checking the state space (all possible behaviors) of software systems is a promising technique for verification and validation. Bugs such as security vulnerabilities, file storage issues, deadlocks and data races can occur anywhere in the state space and are often triggered by corner cases; therefore, it becomes important to explore and model check all runtime choices. However, large and complex software systems generate huge numbers of behaviors leading to 'state explosion'. eXplode is a lightweight, deterministic and depth-bound model checker that explores all dynamic choices at runtime. Given an application-specific test-harness, eXplode performs state search in a serialized fashion - which limits its scalability and performance. This paper proposes a distributed eXplode engine that uses multiple host machines concurrently in order to achieve more state space coverage in less time, and is very helpful to scale up the software verification and validation effort. Test results show that Distributed eXplode runs several times faster and covers more state space than the standalone eXplode.
Subject(s):
Computer science
Item views:
256
Metadata:
text | xml

In Partnership with the Center for Digital Research and Scholarship at Columbia University Libraries/Information Services | Terms of Use