Titel: Semantics-driven extraction of timed automata from Java programs

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.

Publikationstyp: Beitrag in Zeitschrift (Autorenschaft)
Art der Veröffentlichung Online Publikation
Erschienen in: Journal of Empirical Software Engineering (EMSE)
Journal of Empirical Software Engineering (EMSE)
zur Publikation
 ( Springer Verlag GmbH; )
Erscheinungsdatum: 22.03.2019
Titel der Serie: -
Bandnummer: 24
Heftnummer: 5
Erstveröffentlichung: Ja
Version: -
Seite: S. 3114 - 3150


ISSN: 1573-7616
AC-Nummer: -
Open Access
  • Online verfügbar (Open Access)


Organisation Adresse
Fakultät für Technische Wissenschaften
Institut für Informatik-Systeme
Universitätsstr. 65-67
A-9020  Klagenfurt
zur Organisation
Universitätsstr. 65-67
AT - A-9020  Klagenfurt


  • 102022 - Softwareentwicklung
Forschungscluster Kein Forschungscluster ausgewählt
  • Science Citation Index Expanded (SCI Expanded)
Informationen zum Zitationsindex: Master Journal List
Peer Reviewed
  • Ja
  • Science to Science (Qualitätsindikator: I)
Klassifikationsraster der zugeordneten Organisationseinheiten:
  • Software Engineering Research Group


Keine Kooperationspartner ausgewählt

Beiträge der Publikation

Keine verknüpften Publikationen vorhanden