research-article

Modeling time in Java programs for automatic error detection

Authors:

Muhammad Taimoor Khan,

Francesco Spegni,

Andreas Bollin,

Martin PinzgerAuthors Info & Claims

FormaliSE '18: Proceedings of the 6th Conference on Formal Methods in Software Engineering

Pages 50 - 59

https://doi.org/10.1145/3193992.3193997

Published: 02 June 2018 Publication History

Abstract

Modern programming languages, such as Java, represent time as integer variables, called timestamps. Timestamps allow developers to tacitly model incorrect time values resulting in a program failure because any negative value or every positive value is not necessarily a valid time representation. Current approaches to automatically detect errors in programs, such as Randoop and FindBugs, cannot detect such errors because they treat timestamps as normal integer variables and test them with random values verifying if the program throws an exception. In this paper, we present an approach that considers the time semantics of the Java language to systematically detect time related errors in Java programs. With the formal time semantics, our approach determines which integer variables handle time and which statements use or alter their values. Based on this information, it translates these statements into an SMT model that is passed to an SMT solver. The solver formally verifies the correctness of the model and reports the violations of time properties in that program. For the evaluation, we have implemented our approach in a prototype tool and applied it to the source code of 20 Java open source projects. The results show that our approach is scalable and it is capable of detecting time errors precisely enough allowing its usability in real-world applications.

References

[1]

C Artho. 2006. JLint - Find Bugs in Java Programs. (2006). http://jlint.sourceforge.net/.

[2]

Clark Barrett, Aaron Stump, Cesare Tinelli, et al. 2010. The smt-lib standard: Version 2.0. In Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, England), Vol. 13. 14.

[3]

Nikolaj Bjørner and Anh-Dung Phan. 2014. vZ-Maximal Satisfaction with Z3. In In Proceedings of the 6th International Symposium on Symbolic Computation in Software Science (SCSS), Vol. 30. 1--9.

[4]

Nikolaj Bjørner, Anh-Dung Phan, and Lars Fleckenstein. 2015. vZ-An Optimizing SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Vol. 15. Springer, 194--199.

Digital Library

[5]

Denis Bogdanas and Grigore Roşu. 2015. K-Java: A Complete Semantics of Java. In Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 445--456.

Digital Library

[6]

Marat Boshernitsan, Roongko Doong, and Alberto Savoia. 2006. From Daikon to Agitator: lessons and challenges in building a commercial tool for developer testing. In Proceedings of the 2006 international symposium on Software testing and analysis (ISSTA). ACM, 169--180.

Digital Library

[7]

Montgomery Carter, Shaobo He, Jonathan Whitaker, Zvonimir Rakamarić, and Michael Emmi. 2016. SMACK software verification toolchain. In Proceedings of the 38th International Conference on Software Engineering (ICSE). ACM, 589--592.

Digital Library

[8]

Robert N Charette. 2005. Why software fails. IEEE spectrum 42, 9 (2005), 36.

Digital Library

[9]

Tom Copeland. 2005. PMD Applied. Centennial Books.

[10]

Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer, 337--340.

Digital Library

[11]

David Deharbe, Pascal Fontaine, and Bruno Woltzenlogel Paleo. 2011. Quantifier inference rules for SMT proofs. In First International Workshop on Proof eXchange for Theorem Proving (PxTP).

[12]

John Hatcliff and Matthew Dwyer. 2001. Using the Bandera tool set to model-check properties of concurrent Java software. In International Conference on Concurrency Theory (CONCUR). Springer, 39--58.

Digital Library

[13]

Klaus Havelund and Thomas Pressburger. 2000. Model checking java programs using java pathfinder. International Journal on Software Tools for Technology Transfer (STTT) 2, 4 (2000), 366--381.

[14]

Nikolas Havrikov, Alessio Gambi, Andreas Zeller, Andrea Arcuri, and Juan Pablo Galeotti. 2017. Generating unit tests with structured system interactions. In Proceedings of the 12th International Workshop on Automation of Software Testing (AST). IEEE Press, 30--33.

Digital Library

[15]

Thomas A Henzinger, George C Necula, Ranjit Jhala, Gregoire Sutre, Rupak Majumdar, and Westley Weimer. 2002. Temporal-safety proofs for systems code. In International Conference on Computer Aided Verification (CAV). Springer, 526--538.

Digital Library

[16]

Gerard J. Holzmann. 1997. The model checker SPIN. IEEE Transactions on software engineering 23, 5 (1997), 279--295.

Digital Library

[17]

David Hovemeyer and William Pugh. 2004. Finding bugs is easy. ACM Sigplan Notices 39, 12 (2004), 92--106.

Digital Library

[18]

Giovanni Liva, Muhammad Taimoor Khan, and Martin Pinzger. 2017. Extracting timed automata from Java methods. In Proceedings of the 17th International Working Conference on Source Code Analysis and Manipulation (SCAM). IEEE, 91--100.

[19]

Carlos Pacheco and Michael D Ernst. 2005. Eclat: Automatic generation and classification of test inputs. In Proceedings of the 19th European conference on Object-Oriented Programming (ECOOP). Springer-Verlag, 504--527.

Digital Library

[20]

Carlos Pacheco and Michael D Ernst. 2007. Randoop: feedback-directed random testing for Java. In Companion to the 22nd ACM SIGPLAN conference on Object-oriented programming systems and applications companion (OOPSLA). ACM, 815--816.

Digital Library

[21]

Carlos Pacheco, Shuvendu K Lahiri, and Thomas Ball. 2008. Finding errors in. net with feedback-directed random testing. In Proceedings of the 2008 international symposium on Software testing and analysis (ISSTA). ACM, 87--96.

Digital Library

[22]

Carlos Pacheco, Shuvendu K Lahiri, Michael D Ernst, and Thomas Ball. 2007. Feedback-directed random test generation. In Proceedings of the 29th international conference on Software Engineering (ICSE). IEEE Computer Society, 75--84.

Digital Library

[23]

Steven C. Seow. 2008. Designing and Engineering Time: The Psychology of Time Perception in Software (1 ed.). Addison-Wesley Professional.

Digital Library

[24]

Neil Walkinshaw and Kirill Bogdanov. 2008. Inferring finite-state models with temporal constraints. In Proceedings of the IEEE/ACM International Conference on Automated Software Engineering (ASE). IEEE, 248--257.

Digital Library

Cited By

Liva GKhan MPinzger MSpegni FSpalazzi L(2021)Automatic Repair of Timestamp ComparisonsIEEE Transactions on Software Engineering10.1109/TSE.2019.294835147:11(2369-2381)Online publication date: 1-Nov-2021
https://doi.org/10.1109/TSE.2019.2948351
Spegni FSpalazzi LLiva GPinzger MBollin A(2020)Verifying temporal specifications of Java programsSoftware Quality Journal10.1007/s11219-019-09488-9Online publication date: 25-May-2020
https://doi.org/10.1007/s11219-019-09488-9
Liva GKhan MPinzger M(2019)Semantics-driven extraction of timed automata from Java programsEmpirical Software Engineering10.1007/s10664-019-09699-5Online publication date: 22-Mar-2019
https://doi.org/10.1007/s10664-019-09699-5

Index Terms

Modeling time in Java programs for automatic error detection

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

FormaliSE '18: Proceedings of the 6th Conference on Formal Methods in Software Engineering

June 2018

101 pages

ISBN:9781450357180

DOI:10.1145/3193992

General Chairs:
Stefania Gnesi
ISTI-CNR, Italy
,
Nico Plat
Thanos, The Netherlands
,
Program Chairs:
Paola Spoletini
Kennesaw State University
,
Patrizio Pelliccione
Chalmers | University of Gothenburg, Gothenburg, Sweden

Copyright © 2018 ACM.

Permission to make digital or hard copies of all or part 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 components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering
IEEE-CS: Computer Society

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 02 June 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article

Funding Sources

Österreichische Forschungsförderungsgesellschaft

Conference

ICSE '18

Sponsor:

SIGSOFT
IEEE-CS

ICSE '18: 40th International Conference on Software Engineering

June 2, 2018

Gothenburg, Sweden

Upcoming Conference

ICSE 2025

2025 IEEE/ACM 46th International Conference on Software Engineering

April 26 - May 3, 2025

Ottawa , ON , Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
98
Total Downloads

Downloads (Last 12 months)17
Downloads (Last 6 weeks)6

Reflects downloads up to 17 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Liva GKhan MPinzger MSpegni FSpalazzi L(2021)Automatic Repair of Timestamp ComparisonsIEEE Transactions on Software Engineering10.1109/TSE.2019.294835147:11(2369-2381)Online publication date: 1-Nov-2021
https://doi.org/10.1109/TSE.2019.2948351
Spegni FSpalazzi LLiva GPinzger MBollin A(2020)Verifying temporal specifications of Java programsSoftware Quality Journal10.1007/s11219-019-09488-9Online publication date: 25-May-2020
https://doi.org/10.1007/s11219-019-09488-9
Liva GKhan MPinzger M(2019)Semantics-driven extraction of timed automata from Java programsEmpirical Software Engineering10.1007/s10664-019-09699-5Online publication date: 22-Mar-2019
https://doi.org/10.1007/s10664-019-09699-5

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents