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
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},
}Downloads: 3
{"_id":"ivkxJQmBCApm2TFee","bibbaseid":"cassez-jensen-larsen-verificationandparametersynthesisforrealtimeprogramsusingrefinementoftraceabstraction-2021","authorIDs":["aYsqprsgp7HA5GpQ3"],"author_short":["Cassez, F.","Jensen, P. G.","Larsen, K. G."],"bibdata":{"bibtype":"article","type":"article","author":[{"firstnames":["Franck"],"propositions":[],"lastnames":["Cassez"],"suffixes":[]},{"firstnames":["Peter","Gjøl"],"propositions":[],"lastnames":["Jensen"],"suffixes":[]},{"firstnames":["Kim","Guldstrand"],"propositions":[],"lastnames":["Larsen"],"suffixes":[]}],"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","bibtex":"@article{DBLP:journals/fuin/CassezJL21,\n author = {Franck Cassez and\n Peter Gj{\\o}l Jensen and\n Kim Guldstrand Larsen},\n title = {Verification and Parameter Synthesis for Real-Time Programs using\n Refinement of Trace Abstraction},\n journal = {Fundam. Informaticae},\n 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. \nWe 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. \nAll 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.},\n\n volume = {178},\n number = {1-2},\n pages = {31--57},\n year = {2021},\n url = {https://doi.org/10.3233/FI-2021-1997},\n doi = {10.3233/FI-2021-1997},\n timestamp = {Fri, 22 Jan 2021 00:00:00 +0100},\n biburl = {https://dblp.org/rec/journals/fuin/CassezJL21.bib},\n bibsource = {dblp computer science bibliography, https://dblp.org},\n urlpaper = {papers/fi-2021.pdf},\n}\n\n","author_short":["Cassez, F.","Jensen, P. G.","Larsen, K. G."],"key":"DBLP:journals/fuin/CassezJL21","id":"DBLP:journals/fuin/CassezJL21","bibbaseid":"cassez-jensen-larsen-verificationandparametersynthesisforrealtimeprogramsusingrefinementoftraceabstraction-2021","role":"author","urls":{"Paper":"https://franck44.github.io/publications/papers/fi-2021.pdf"},"metadata":{"authorlinks":{"cassez, f":"http://science.mq.edu.au/~fcassez/software-verif.html"}},"downloads":3,"html":""},"bibtype":"article","biburl":"https://franck44.github.io/publications/franck-pubs.bib","creationDate":"2021-02-14T22:28:51.287Z","downloads":3,"keywords":[],"search_terms":["verification","parameter","synthesis","real","time","programs","using","refinement","trace","abstraction","cassez","jensen","larsen"],"title":"Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction","year":2021,"dataSources":["8742EsvjQfyP2fYBW"]}