\textsf{IMITATOR} 3: synthesis of timing parameters beyond decidability

DOI10.1007/978-3-030-81685-8_26MaRDI QIDQ832203zbMATH OpenOpenAlexFDO

Authors Étienne André

Publication date 25 March 2022

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-81685-8_26

zbMATH Keywords

parameter synthesisparametric timed automatareal-time systems

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Synthesis of timing parameters satisfying safety properties
• Real-Time Model-Checking: Parameters everywhere
• Parametric timing analysis for real-time systems
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• Bounded Model Checking for Parametric Timed Automata

Cites work

• A theory of timed automata
• Behavioral cartography of timed automata
• Event-clock automata: a determinizable class of timed automata
• scientific article; zbMATH DE number 1759608 (Why is no real title available?)
• HyTech: A model checker for hybrid systems
• Iterative bounded synthesis for efficient cycle detection in parametric timed automata
• Language emptiness of continuous-time parametric timed automata
• Language preservation problems in parametric timed automata
• Learning-based compositional parameter synthesis for event-recording automata
• Merge and conquer: state merging in parametric timed automata
• Parametric analyses of attack-fault trees
• Parametric Deadlock-Freeness Checking Timed Automata
• Parametric model-checking of stopwatch Petri nets
• Parametric real-time reasoning
• Parametric schedulability analysis of a launcher flight control system under reactivity constraints
• Parametric Timed Model Checking for Guaranteeing Timed Opacity
• Parametric updates in parametric timed automata
• PPLite: zero-overhead encoding of NNC polyhedra
• The algorithmic analysis of hybrid systems
• The power of reachability testing for timed automata
• Timed verification of the generic architecture of a memory circuit using parametric timed automata
• Uppaal in a nutshell
• Verification of an industrial asynchronous leader election algorithm using abstractions and parametric model checking

Cited in

(6)

• Zone-based verification of timed automata: extrapolations, simulations and what next?
• Efficient convex zone merging in parametric timed automata
• Synthesis of timing parameters satisfying safety properties
• A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets
• Formal analysis of real-time systems with user-defined strategies in rewriting logic
• Dense integer-complete synthesis for bounded parametric timed automata

Describes a project that uses

Uses Software

• IMITATOR
• HyTech
• Uppaal
• PPL
• SpaceEx
• GitHub

This page was built for publication: \textsf{IMITATOR} 3: synthesis of timing parameters beyond decidability

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