Publikation: Modeling Time in Java Programs for Auto...
Stammdaten
Titel: | 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) |
Erscheinungsdatum: | 02.06.2018 (Online) |
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
(
ACM New York;
)
zur Publikation |
Titel der Serie: | - |
Bandnummer: | - |
Erstveröffentlichung: | Ja |
Version: | - |
Seite: | S. 50 - 59 |
Versionen
Keine Version vorhanden |
Erscheinungsdatum: | 02.06.2018 |
ISBN (e-book): |
|
eISSN: | - |
DOI: | http://dx.doi.org/10.1145/3193992.3193997 |
Homepage: | https://dl.acm.org/citation.cfm?id=3193997 |
Open Access |
|
AutorInnen
Giovanni Liva (intern) | ||||
Muhammad Taimoor Khan (intern) | ||||
Francesco Spegni
|
||||
Luca Spalazzi
|
||||
Martin Pinzger (intern) | ||||
Andreas Bollin (intern) |
Zuordnung
Organisation | Adresse | ||||
---|---|---|---|---|---|
Fakultät für Technische Wissenschaften
Institut für Informatik-Systeme
|
AT - A-9020 Klagenfurt |
||||
Fakultät für Technische Wissenschaften
Institut für Informatikdidaktik
|
AT - A-9020 Klagenfurt |
Kategorisierung
Sachgebiete | |
Forschungscluster | Kein Forschungscluster ausgewählt |
Peer Reviewed |
|
Publikationsfokus |
Klassifikationsraster der zugeordneten Organisationseinheiten:
|
Arbeitsgruppen |
|
Kooperationen
Organisation | Adresse | ||
---|---|---|---|
Università Politecnica delle Marche (UNIVPM)
|
IT - 60121 Ancona |
Forschungsaktivitäten
(Achtung: Externe Aktivitäten werden im Suchergebnis nicht mitangezeigt)
Projekte: |
|
Publikationen: | Keine verknüpften Publikationen vorhanden |
Veranstaltungen: | Keine verknüpften Veranstaltung vorhanden |
Vorträge: | Keine verknüpften Vorträge vorhanden |