Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction. Cassez, F., Jensen, P. G., & Larsen, K. G. Fundam. Informaticae, 178(1-2):31–57, 2021. ![Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction [pdf]](https://bibbase.org/img/filetypes/pdf.svg "pdf")
Paper doi abstract bibtex 3 downloads We address the safety verification and synthesis problems for real-time systems. We introduce real-time programs that are made of instructions that can perform assignments to discrete and real-valued variables. They are general enough to capture interesting classes of timed systems such as timed automata, stopwatch automata, time(d) Petri nets and hybrid automata. We propose a semi-algorithm using refinement of trace abstractions to solve both the reachability verification problem and the parameter synthesis problem for real-time programs. All of the algorithms proposed have been implemented and we have conducted a series of experiments, comparing the performance of our new approach to state-of-the-art tools in classical reachability, robustness analysis and parameter synthesis for timed systems. We show that our new method provides solutions to problems which are unsolvable by the current state-of-the-art tools.
@article{DBLP:journals/fuin/CassezJL21,
author = {Franck Cassez and
Peter Gj{\o}l Jensen and
Kim Guldstrand Larsen},
title = {Verification and Parameter Synthesis for Real-Time Programs using
Refinement of Trace Abstraction},
journal = {Fundam. Informaticae},
abstract = {We address the safety verification and synthesis problems for real-time systems. We introduce real-time programs that are made of instructions that can perform assignments to discrete and real-valued variables. They are general enough to capture interesting classes of timed systems such as timed automata, stopwatch automata, time(d) Petri nets and hybrid automata.
We propose a semi-algorithm using refinement of trace abstractions to solve both the reachability verification problem and the parameter synthesis problem for real-time programs.
All of the algorithms proposed have been implemented and we have conducted a series of experiments, comparing the performance of our new approach to state-of-the-art tools in classical reachability, robustness analysis and parameter synthesis for timed systems. We show that our new method provides solutions to problems which are unsolvable by the current state-of-the-art tools.},
volume = {178},
number = {1-2},
pages = {31--57},
year = {2021},
url = {https://doi.org/10.3233/FI-2021-1997},
doi = {10.3233/FI-2021-1997},
timestamp = {Fri, 22 Jan 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/fuin/CassezJL21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
urlpaper = {papers/fi-2021.pdf},
}