Stammdaten

Modeling Time in Java Programs for Automatic Error Detection
Untertitel:
Kurzfassung:

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.

Schlagworte:
Publikationstyp: Beitrag in Proceedings (Autorenschaft)
Art der Veröffentlichung Online Publikation
Erschienen in: FormaliSE '18 Proceedings of the 6th Conference on Formal Methods in Software Engineering
FormaliSE '18 Proceedings of the 6th Conference on Formal Methods in Software Engineering
zur Publikation
 ( ACM New York; )
Erscheinungdatum: 02.06.2018
Titel der Serie: -
Bandnummer: -
Erstveröffentlichung: Ja
Version: -
Seite: S. 50 - 59

Identifikatoren

ISBN:
  • 978-1-4503-5718-0
ISSN: -
DOI: http://dx.doi.org/10.1145/3193992.3193997
AC-Nummer: -
Homepage: https://dl.acm.org/citation.cfm?id=3193997
Open Access
  • Online verfügbar (nicht Open Access)

Zuordnung

Organisation Adresse
Fakultät für Technische Wissenschaften
 
Institut für Informatik-Systeme
Universitätsstr. 65-67
A-9020  Klagenfurt
Österreich
  -993502
   sek-eder@isys.uni-klu.ac.at
https://www.aau.at/isys/
zur Organisation
Universitätsstr. 65-67
AT - A-9020  Klagenfurt
Fakultät für Technische Wissenschaften
 
Institut für Informatikdidaktik
Universitätsstr. 65-67
A-9020  Klagenfurt
Österreich
https://iid.aau.at/
zur Organisation
Universitätsstr. 65-67
AT - A-9020  Klagenfurt

Kategorisierung

Sachgebiete
  • 101013 - Mathematische Logik
  • 102022 - Softwareentwicklung
Forschungscluster Kein Forschungscluster ausgewählt
Peer Reviewed
  • Ja
Publikationsfokus
  • Science to Science (Qualitätsindikator: II)
Klassifikationsraster der zugeordneten Organisationseinheiten:
Arbeitsgruppen
  • Software Engineering Research Group

Kooperationen

Organisation Adresse
Università Politecnica delle Marche (UNIVPM)
P.zza Roma 22
60121  Ancona
Italien
P.zza Roma 22
IT - 60121  Ancona

Beiträge der Publikation

Keine verknüpften Publikationen vorhanden