论文标题
使用痕量抽象的完善实时程序的验证和参数合成
Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction
论文作者
论文摘要
我们解决了实时系统的安全验证和合成问题。我们介绍了由指令制成的实时程序，这些程序可以执行分配和实现变量的作业。它们足够一般，可以捕获有趣的定时系统类别，例如定时自动机，秒表自动机，时间（D）Petri Nets和Hybrid Automata。 我们使用痕量抽象的细化提出了一个半合理，以解决实时程序的可及性验证问题和参数综合问题。 提出的所有算法都已实施，我们进行了一系列实验，比较了我们对定时系统的经典可及性，鲁棒性分析和参数合成的新方法的性能。我们表明，我们的新方法为问题提供了解决方案，这些问题无法通过当前的最新工具无法解决。
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.
