Publikation: Verifying temporal specifications of Ja...
Stammdaten
Titel: | Verifying temporal specifications of Java programs |
Untertitel: | |
Kurzfassung: | Many Java programs encode temporal behaviors in their source code, typically mixing three features provided by the Java language: (1) pausing the execution for a limited amount of time, (2) waiting for an event that has to occur before a deadline expires, and (3) comparing timestamps. In this work, we show how to exploit modern SMT solvers together with static analysis in order to produce a network of timed automata approximating the temporal behavior of a set of Java threads. We also prove that the presented abstraction preserves the truth of MTL and ATCTL formulae, two well-known logics for expressing timed specifications. As far as we know, this is the first feasible approach enabling the user to automatically model check timed specifications of Java software directly from the source code. |
Schlagworte: | Software model checking, Time-dependent behavior, Java, Timed automata, SMT, Predicate abstraction |
Publikationstyp: | Beitrag in Zeitschrift (Autorenschaft) |
Erscheinungsdatum: | 02.07.2020 (Print) |
Erschienen in: |
Software Quality Journal
Software Quality Journal
(
Springer;
R. Harrison
)
zur Publikation |
Titel der Serie: | - |
Bandnummer: | 28 |
Heftnummer: | - |
Erstveröffentlichung: | Ja |
Seite: | S. 695 - 744 |
Versionen
Keine Version vorhanden |
Erscheinungsdatum: | 02.07.2020 |
ISBN: | - |
ISSN: | 0963-9314 |
Homepage: | - |
AutorInnen
Francesco Spegni
|
||||
Luca Spalazzi
|
||||
Giovanni Liva (intern) | ||||
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 |
Zitationsindex |
Informationen zum Zitationsindex: Master Journal List
|
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 |