Liva, Giovanni ORCID: https://orcid.org/0000-0002-9337-5762, Khan, Muhammad Taimoor ORCID: https://orcid.org/0000-0002-5752-6420 and Pinzger, Martin (2019) Semantics-driven extraction of timed automata from Java programs. Empirical Software Engineering, 24 (5). pp. 3114-3150. ISSN 1382-3256 (Print), 1573-7616 (Online) (doi:10.1007/s10664-019-09699-5)

Preview

PDF (OA Article) 24374 KHAN_Semantics-driven_Extraction_Timed_Automata_Java_Programs_(OA)_2019.pdf - Published Version Available under License Creative Commons Attribution. Download (2MB) | Preview

Abstract

The automatic verification of time properties of models extracted from programs is challenging, mainly because modern programming languages, such as Java, represent time without a proper semantics. Current approaches to extract time models from source code either represent time only as a tree-like sequence of events or require developers to manually provide a formal model of the time behavior. This makes it difficult for software developers to verify various aspects of their systems, such as timeouts, delays and periodicity of the execution. In this paper, we introduce a formal definition of the time semantics for the Java programming language. Based on the semantics, we present an approach to automatically extract timed automata and their time constraints from Java programs at method level. First, our approach detects the Java statements that involve time, from which it then extracts the timed automata. Our extracted automata are directly amenable to the verification of time properties of the corresponding Java methods. We evaluated the accuracy of our approach on twenty open source Java projects that implement time behavior in their source code. The results show that our approach achieves 100% precision and recall in identifying time related information. They also show that 95% of the timed automata extracted from source code correctly model the time behavior of the method. Finally, we show the applicability of our timed automata to identify eight real errors in four open source Apache systems.

Item Type:	Article
Uncontrolled Keywords:	program verification, time semantics, timed automata
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/24374

Actions (login required)

View Item

Downloads