Verification and parameter synthesis for real-time programs using refinement of trace abstraction

DOI10.3233/FI-2021-1997zbMATH Open1478.68053arXiv2007.10539MaRDI QIDQ4989166FDOQ4989166

Authors: Franck Cassez, Larsen Kim Guldstrand, Peter Gjøl Jensen 

Publication date: 21 May 2021

Published in: Fundamenta Informaticae (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/2007.10539

Recommendations

• Refinement of trace abstraction for real-time programs
• Parameter synthesis for hierarchical concurrent real-time systems
• Synthesis of timing parameters satisfying safety properties
• Verification, refinement and scheduling of real-time programs
• Integer-complete synthesis for bounded parametric timed automata

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Hybrid Systems: Computation and Control
• A theory of timed automata
• What's decidable about hybrid automata?
• Title not available (Why is that?)
• Title not available (Why is that?)
• The expressive power of time Petri nets
• Infinite-state invariant checking with IC3 and predicate abstraction
• Formal Modeling and Analysis of Timed Systems
• Trace Abstraction Refinement for Timed Automata
• Automatic Abstraction Refinement for Timed Automata
• Abstractions for hybrid systems
• Symbolic quantitative robustness analysis of timed automata
• A Counterexample-Guided Approach to Parameter Synthesis for Linear Hybrid Automata
• An iterative approach to precondition inference using constrained Horn clauses
• Refinement of Trace Abstraction
• Title not available (Why is that?)
• Verification of Concurrent Programs Using Trace Abstraction Refinement
• Refinement of trace abstraction for real-time programs
• Tools and algorithms for the construction and analysis of systems. 25 years of TACAS: TOOLympics, held as part of ETAPS 2019, Prague, Czech Republic, April 6--11, 2019. Proceedings. Part III
• TCTL-preserving translations from timed-arc Petri nets to networks of timed automata
• Title not available (Why is that?)

Cited In (2)

• Trace Abstraction-Based Verification for Uninterpreted Programs
• Timed automata verification and synthesis via finite automata learning

Uses Software

• IMITATOR
• PHAVer
• HyTech
• Uppaal
• z3
• SpaceEx

This page was built for publication: Verification and parameter synthesis for real-time programs using refinement of trace abstraction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4989166)