jpf-logic: a Framework for Checking Temporal Logic Properties of Java Code
We present jpf-logic. It is an extension of Java PathFinder (JPF), a model checker for Java apps. Our extension jpf-logic provides a framework to check properties expressed in temporal logics such a linear temporal logic (LTL) and computation tree logic (CTL). To support a logic in our framework, one has to implement a parser for the logic, one has to develop a hierarchy of classes that represent the abstract syntax of the logic and implement a transformation from parse trees of formulas to the corresponding abstract syntax trees, and one has to implement a model checking algorithm that takes as input an abstract syntax tree of a formula and a partial transition system. The latter represents a model of the Java app. All three components have been implemented for CTL. The first two have been implemented for LTL.
In this work, we conduct a study about SPF’s existing string support by running tests on a version of SPF with the latest string support. Base on the results, we then analyze each string method and identify the major challenges in supporting them. We categorize string API functions by type of the challenge, propose several solutions to each of the challenges, and discuss the feasibility and disadvantages of different approaches. We implement support in the case of three string methods according to the proposed solution, leaving other methods as future work.
