Skip navigation

Modeling time in Java programs for automatic error detection

Modeling time in Java programs for automatic error detection

Liva, Giovanni, Khan, Muhammad Taimoor, Spegni, Francesco, Spalazzi, Luca, Bollin, Andreas and Pinzger, Martin (2018) Modeling time in Java programs for automatic error detection. In: Proceedings of the 6th Conference on Formal Methods in Software Engineering - FormaliSE '18. ACM, New York, USA, pp. 50-59. ISBN 978-1450357180 (doi:https://doi.org/10.1145/3193992.3193997)

[img]
Preview
PDF (Author's Accepted Manuscript)
24377 KHAN_Modeling_Java_Programs_Automatic_Error_Detection_(AAM)_2018.pdf - Accepted Version

Download (670kB) | Preview

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.

Item Type: Conference Proceedings
Title of Proceedings: Proceedings of the 6th Conference on Formal Methods in Software Engineering - FormaliSE '18
Additional Information: 40th International Conference on Software Engineering (ICSE) collocated FormlalSE
Uncontrolled Keywords: Java, semantics, computer bugs, tools, software, runtime
Subjects: Q Science > QA Mathematics > QA75 Electronic computers. Computer science
Faculty / Department / Research Group: Faculty of Liberal Arts & Sciences
Faculty of Liberal Arts & Sciences > Department of Computing & Information Systems
Faculty of Liberal Arts & Sciences > Internet of Things and Security (ISEC)
Last Modified: 28 Nov 2019 15:50
Selected for GREAT 2016: None
Selected for GREAT 2017: None
Selected for GREAT 2018: None
Selected for GREAT 2019: GREAT 2
URI: http://gala.gre.ac.uk/id/eprint/24377

Actions (login required)

View Item View Item

Downloads

Downloads per month over past year

View more statistics