Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction

TL;DR

This paper presents a semi-algorithm based on trace abstraction refinement for verifying safety and synthesizing parameters in real-time systems, capable of handling complex timed automata and hybrid models.

Contribution

It introduces a novel semi-algorithm for verification and parameter synthesis in real-time programs, outperforming existing tools on complex timed systems.

Findings

Successfully verified safety properties of complex timed automata.

Achieved parameter synthesis for systems unsolvable by current methods.

Demonstrated improved performance over state-of-the-art tools.

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.