Publication: Verifying temporal specifications of Ja...
Master data
Title: | Verifying temporal specifications of Java programs |
Subtitle: | |
Abstract: | 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. |
Keywords: | Software model checking, Time-dependent behavior, Java, Timed automata, SMT, Predicate abstraction |
Publication type: | Article in journal (Authorship) |
Publication date: | 02.07.2020 (Print) |
Published by: |
Software Quality Journal
Software Quality Journal
(
Springer;
R. Harrison
)
to publication |
Title of the series: | - |
Volume number: | 28 |
Issue: | - |
First publication: | Yes |
Page: | pp. 695 - 744 |
Versionen
Keine Version vorhanden |
Publication date: | 02.07.2020 |
ISBN: | - |
ISSN: | 0963-9314 |
Homepage: | - |
Authors
Francesco Spegni
|
||||
Luca Spalazzi
|
||||
Giovanni Liva (internal) | ||||
Martin Pinzger (internal) | ||||
Andreas Bollin (internal) |
Assignment
Organisation | Address | ||||
---|---|---|---|---|---|
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 |
Categorisation
Subject areas | |
Research Cluster | No research Research Cluster selected |
Citation index |
Information about the citation index: Master Journal List
|
Peer reviewed |
|
Publication focus |
Classification raster of the assigned organisational units:
|
working groups |
|
Cooperations
Organisation | Address | ||
---|---|---|---|
Università Politecnica delle Marche (UNIVPM)
|
IT - 60121 Ancona |
Research activities
Projects: |
|
Publications: | No related publications |
Events: | No related events |
Lectures: | No related lectures |