Symbolic Robustness Analysis of Timed Automata

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

Fundamenta Informaticae ◽

10.3233/fi-2021-1997 ◽

2021 ◽

Vol 178 (1-2) ◽

pp. 31-57

Author(s):

Franck Cassez ◽

Peter Gjøl Jensen ◽

Kim Guldstrand Larsen

Keyword(s):

Real Time ◽

State Of The Art ◽

Timed Automata ◽

Robustness Analysis ◽

Hybrid Automata ◽

Timed Systems ◽

Current State ◽

Parameter Synthesis ◽

Series Of Experiments ◽

Time Systems

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.

Download Full-text

Quantitative Robustness Analysis of Flat Timed Automata

Foundations of Software Science and Computational Structures - Lecture Notes in Computer Science ◽

10.1007/978-3-642-19805-2_16 ◽

2011 ◽

pp. 229-244 ◽

Cited By ~ 10

Author(s):

Rémi Jaubert ◽

Pierre-Alain Reynier

Keyword(s):

Timed Automata ◽

Robustness Analysis

Download Full-text

IMITATOR 3: Synthesis of Timing Parameters Beyond Decidability

Computer Aided Verification - Lecture Notes in Computer Science ◽

10.1007/978-3-030-81685-8_26 ◽

2021 ◽

pp. 552-565

Author(s):

Étienne André

Keyword(s):

Model Checking ◽

Real Time ◽

Timed Automata ◽

Robustness Analysis ◽

Parametric Model ◽

Timing Constraints ◽

Real Time Systems ◽

Model Checker ◽

Time Systems ◽

Timed Model Checking

AbstractReal-time systems are notoriously hard to verify due to nondeterminism, concurrency and timing constraints. When timing constants are uncertain (in early the design phase, or due to slight variations of the timing bounds), timed model checking techniques may not be satisfactory. In contrast, parametric timed model checking synthesizes timing values ensuring correctness. takes as input an extension of parametric timed automata (PTAs), a powerful formalism to formally verify critical real-time systems. extends PTAs with multi-rate clocks, global rational-valued variables and a set of additional useful features. We describe here the new features and algorithms offered by 3, that moved along the years from a simple prototype dedicated to robustness analysis to a standalone parametric model checker for timed systems.

Download Full-text