Parameter synthesis for hierarchical concurrent real-time systems

DOI10.1007/s11241-014-9208-6zbMath1314.68081OpenAlexW2068710718MaRDI QIDQ488231

Yang Liu, Jun Sun, Jin-Song Dong, Étienne André

Publication date: 23 January 2015

Published in: Real-Time Systems (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/10072/172887

zbMATH Keywords

robustnessmodel checkingparametric timed verificationreal-time specification

Mathematics Subject Classification ID

Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Distributed parametric model checking timed automata under non-zenoness assumption ⋮ PSyHCoS

Uses Software

• IMITATOR
• VINAS-P
• TREX
• HyTech
• Uppaal
• PPL
• Shrinktech
• PAT

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The octahedron abstract domain
• Timed verification of the generic architecture of a memory circuit using parametric timed automata
• Decision problems for lower/upper bound parametric timed automata
• A theory of timed automata
• Symbolic model checking for real-time systems
• HyTech: A model checker for hybrid systems
• Uppaal in a nutshell
• Linear parametric model checking of timed automata
• Scheduling with timed automata
• Precise Robustness Analysis of Time Petri Nets with Inhibitor Arcs
• Time Separation of Events: An Inverse Method
• Bounded Model Checking for Parametric Timed Automata
• Quantitative Robustness Analysis of Flat Timed Automata
• Timed Automata Can Always Be Made Implementable
• Robust Reachability in Timed Automata: A Game-Based Approach
• Behavioral Cartography of Timed Automata
• AN INVERSE METHOD FOR PARAMETRIC TIMED AUTOMATA
• Specification and Proof in Real Time CSP
• On the power of non-observable actions in timed automata
• Robustness of Time Petri Nets under Guard Enlargement
• Merge and Conquer: State Merging in Parametric Timed Automata
• Robustness in Timed Automata
• Parametric real-time reasoning
• Integer Parameter Synthesis for Timed Automata
• Formal Methods for the Design of Real-Time Systems
• Lectures on Concurrency and Petri Nets
• Formal Modeling and Analysis of Timed Systems
• Integrated Formal Methods