Nastaran Shafiei
ABSTRACT
Java PathFinder (JPF) is a model checker for Java applications. Despite its maturity, JPF cannot be used to verify any realistic Java application without a nontrivial amount of work done by its user. One of the main limiting factors towards model checking such applications is handling native calls. JPF provides ways for users to handle such calls. However, those require modeling the behaviour of the native methods in Java which is labour intensive and hinders the uptake of JPF by developers. This paper presents our tool that extends JPF to address this problem. Our work alleviates this burden for users by automatically handling native calls. Our approach is based on delegating the execution of native calls from JPF to their original execution environment. We showcase our extension by applying it to a variety of simple yet realistic Java applications that JPF, without our extension, cannot handle.
- C. Artho, W. Leungwattanakit, M. Hagiya, and Y. Tanabe. Efficient model checking of networked applications. In TOOLS, 2008.Google Scholar
Cross Ref
- E. D. Barlas and T. Bultan. NetStub: a framework for verification of distributed Java applications. In ASE, 2007. Google ScholarDigital Library
- T. Brown and J. Helga. Non-blocking k-ary search trees. In OPODIS, 2011. Google ScholarDigital Library
- C. Cadar, D. Dunbar, and D. Engler. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI, 2008. Google ScholarDigital Library
- J. d. Halleux and N. Tillmann. Moles: tool-assisted environment isolation with closures. In TOOLS, 2010. Google ScholarDigital Library
- M. d’Amorim, A. Sobeih, and D. Marinov. Optimized execution of deterministic blocks in Java PathFinder. In ICFEM, 2006. Google ScholarDigital Library
- P. Godefroid, J. D. Herbsleb, L. J. Jagadeesan, and D. Li. Ensuring privacy in presence awareness systems: an automated verification approach. In CSCW, 2000. Google ScholarDigital Library
- S. Liang. The Java native interface: programmer’s guide and specification. 1999. Google ScholarDigital Library
- N. Shafiei and F. v. Breugel. Towards model checking of computer games with Java PathFinder. In GAS, 2013.Google ScholarCross Ref
- M. Ujma and N. Shafiei. jpf-concurrent: an extension of Java PathFinder for java.util.concurrent. In JPF Workshop, 2011.Google Scholar
Index Terms
- Automatic handling of native methods in Java PathFinder
Recommendations
Verifying android applications using Java PathFinder
Mobile application testing is a specialised and complex field. Due to mobile applications' event driven design and mobile runtime environment, there currently exist only a small number of tools to verify these applications. This paper describes the ...
Tools to generate and check consistency of model classes for Java PathFinder
Java PathFinder (JPF) is a model checker for Java applications. Like any other model checker, JPF has to combat the notorious state space explosion problem. Since JPF is a JVM, it can only model check Java bytecode and needs to handle native calls ...
State extensions for java pathfinder
ICSE '08: Proceedings of the 30th international conference on Software engineeringJava PathFinder (JPF) is an explicit-state model checker for Java programs. JPF implements a backtrackable Java Virtual Machine (JVM) that provides non-deterministic choices and control over thread scheduling. JPF is itself implemented in Java and runs ...
Comments