Liva, Giovanni, Khan, Muhammad Taimoor ORCID: https://orcid.org/0000-0002-5752-6420, 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:10.1145/3193992.3193997)

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 / School / Research Centre / Research Group:	Faculty of Engineering & Science > Internet of Things and Security Research Centre (ISEC) Faculty of Engineering & Science > School of Computing & Mathematical Sciences (CMS) Faculty of Engineering & Science
Last Modified:	04 Mar 2022 13:06
URI:	http://gala.gre.ac.uk/id/eprint/24377

Actions (login required)

View Item

Downloads