WCSE

Model Checking Java Programs with JPSL

Abstract— In order to solve the verification problem of Java programs, a novel model checking approach with JPSL (Java Property Specification Language) is advocated. To this end, the JPSL is defined for describing the desired properties of Java programs with a specific format of annotation mixed into the source code, and the technique for automatically converting the JPSL properties into their equivalent PPTL (Propositional Projection Temporal Logic) formulas is formalize, which in turn can be directly used to model checking Java programs with MSV tool. In addition, an example is given to illustrate how the approach works. The approach provides a convenient and powerful way for engineers to verify Java programs, and helps to improve the quality of the software system.

Index Terms— JPSL, Java, program verification, model checking.

Xinfeng Shu
School of Computer Science and Technology, Xi'an University of Posts and Telecommunications, China
Gege Quan
School of Computer Science and Technology, Xi'an University of Posts and Telecommunications, China

[Download]

Cite: Xinfeng Shu, Gege Quan, " Model Checking Java Programs with JPSL, " WCSE 2022 Spring Event: 2022 9th International Conference on Industrial Engineering and Applications, pp. 1521-1530, Sanya, China, April 15-18, 2022.