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 |
Externí odkaz: |
načítá se...