Ranged Model Checking

Autor: Junaid Haroon Siddiqui, Diego Funes, Sarfraz Khurshid
Rok vydání: 2012
Předmět:
Zdroj: ACM SIGSOFT Software Engineering Notes. 37:1-5
ISSN: 0163-5948
DOI: 10.1145/2382756.2382799
Popis: We introduce ranged model checking, a novel technique for more effective checking of Java programs using the Java PathFinder (JPF) model checker. Our key insight is that the order in which JPF makes non-deterministic choices denes a total ordering of execution paths it explores in the program it checks. Thus, two in-order paths define a range for restricting the model checking run by defining a start point and an end point for JPF's exploration. Moreover, a given set of paths can be linearly ordered to define consecutive, (essentially) non-overlapping ranges that partition the exploration space and can be explored separately. While restricting the run of a model checker is a well-known technique in model checking, the key novelty of our work is conceptually to restrict the run using vertical boundaries rather than the traditional approach of using a horizontal boundary, i.e., the search depth bound. Initial results using our prototype implementation using the JPF libraries demonstrate the promise ranged model checking holds.
Databáze: OpenAIRE
načítá se...