Back to Search
Start Over
Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction*.
- Source :
-
Fundamenta Informaticae . 2021, Vol. 178 Issue 1/2, p31-57. 27p. - Publication Year :
- 2021
-
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. [ABSTRACT FROM AUTHOR]
- Subjects :
- *MACHINE theory
*HYBRID systems
*PETRI nets
*ALGORITHMS
Subjects
Details
- Language :
- English
- ISSN :
- 01692968
- Volume :
- 178
- Issue :
- 1/2
- Database :
- Academic Search Index
- Journal :
- Fundamenta Informaticae
- Publication Type :
- Academic Journal
- Accession number :
- 148108092
- Full Text :
- https://doi.org/10.3233/FI-2021-1997