eduzhai > Applied Sciences > Engineering >

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

  • king
  • (0) Download
  • 20210506
  • Save

... pages left unread,continue reading

Document pages: 30 pages

Abstract: We address the safety verification and synthesis problems for real-timesystems. We introduce real-time programs that are made of instructions that canperform assignments to discrete and real-valued variables. They are generalenough 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 solveboth the reachability verification problem and the parameter synthesis problemfor real-time programs.All of the algorithms proposed have been implemented and we have conducted aseries of experiments, comparing the performance of our new approach tostate-of-the-art tools in classical reachability, robustness analysis andparameter synthesis for timed systems. We show that our new method providessolutions to problems which are unsolvable by the current state-of-the-arttools.

Please select stars to rate!

         

0 comments Sign in to leave a comment.

    Data loading, please wait...
×