[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
article

jpf-logic: a Framework for Checking Temporal Logic Properties of Java Code

Published: 17 January 2023 Publication History

Abstract

We present jpf-logic, an extension of the model checker Java PathFinder (JPF). Our extension jpf-logic provides a framework to check properties expressed in temporal logics such as linear temporal logic (LTL) and computation tree logic (CTL). To support a logic in our framework, we (1) implement a parser for the logic, (2) 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 (3) 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 application. All three components have been implemented for CTL. The first two have been implemented for LTL.

References

[1]
Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. The MIT Press, Cambridge, MA, USA, 2008.
[2]
Franck van Breugel. Java PathFinder: a tool to detect bugs in Java code. 2020.
[3]
Glenn Bruns and Patrice Godefroid. Model checking partial state spaces with 3-valued temporal logics. In Nicolas Halbwachs and Doron Peled, editors, Proceedings of the 11th International Conference on Computer Aided Verification, volume 1633 of Lecture Notes in Computer Science, Trento, Italy, July 1999. Springer-Verlag.
[4]
Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Dexter Kozen, editor, Proceedings of the Workshop on Logics of Programs, volume 131 of Lecture Notes in Computer Science, pages 52--71, Yorktown Heights, NY, USA, May 1981. Springer-Verlag.
[5]
Syyeda Zainab Fatmi. Probabilistic model checking of randomized Java code. Master's thesis, York University, Toronto, Canada, September 2020.
[6]
Watcharin Leungwattanakit, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto, and Koichi Takahashi. Modular software model checking for distributed systems. IEEE Transactions on Software Engineering, 40(5):483--501, May 2014.
[7]
Terence Parr. The Definitive ANTLR 4 Reference. The Pragmatic Bookshelf, Dallas, TX, USA, 2013.
[8]
Amir Pnueli. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science, pages 46--57, Providence, RI, USA, October/November 1977. IEEE.
[9]
Willem Visser, Klaus Havelund, Guillaume Brat, Seungjoon Park, and Flavio Lerda. Model checking programs. Automated Software Engineering, 10(2):203--232, April 2003.

Cited By

View all
  • (2024)SpecBCFuzz: Fuzzing LTL Solvers with Boundary ConditionsProceedings of the IEEE/ACM 46th International Conference on Software Engineering10.1145/3597503.3639087(1-13)Online publication date: 20-May-2024
  • (2024)JPF: From 2003 to 2023Tools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57249-4_1(3-22)Online publication date: 6-Apr-2024

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGSOFT Software Engineering Notes
ACM SIGSOFT Software Engineering Notes  Volume 48, Issue 1
January 2023
113 pages
ISSN:0163-5948
DOI:10.1145/3573074
Issue’s Table of Contents
Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 17 January 2023
Published in SIGSOFT Volume 48, Issue 1

Check for updates

Qualifiers

  • Article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)14
  • Downloads (Last 6 weeks)2
Reflects downloads up to 12 Dec 2024

Other Metrics

Citations

Cited By

View all
  • (2024)SpecBCFuzz: Fuzzing LTL Solvers with Boundary ConditionsProceedings of the IEEE/ACM 46th International Conference on Software Engineering10.1145/3597503.3639087(1-13)Online publication date: 20-May-2024
  • (2024)JPF: From 2003 to 2023Tools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57249-4_1(3-22)Online publication date: 6-Apr-2024

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media