Parameter synthesis for hierarchical concurrent real-time systems

DOI10.1007/S11241-014-9208-6zbMATH Open1314.68081OpenAlexW2068710718MaRDI QIDQ488231FDOQ488231

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

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

Recommendations

• Parametric timing analysis for real-time systems
• Robust synthesis for real-time systems
• scientific article; zbMATH DE number 3868590
• Toward parametric timed interfaces for real-time components
• Algorithm for synthesis of real-time systems under reliability constraints

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)

Cites Work

• HyTech: A model checker for hybrid systems
• Uppaal in a nutshell
• Title not available (Why is that?)
• Title not available (Why is that?)
• A theory of timed automata
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• On the power of non-observable actions in timed automata
• Title not available (Why is that?)
• Formal Methods for the Design of Real-Time Systems
• Lectures on Concurrency and Petri Nets
• Symbolic model checking for real-time systems
• Title not available (Why is that?)
• Parametric model-checking of stopwatch Petri nets
• AN INVERSE METHOD FOR PARAMETRIC TIMED AUTOMATA
• Parametric real-time reasoning
• Decision problems for lower/upper bound parametric timed automata
• Linear parametric model checking of 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
• Specification and Proof in Real Time CSP
• Title not available (Why is that?)
• Integrated Formal Methods
• The octahedron abstract domain
• Timed verification of the generic architecture of a memory circuit using parametric 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
• Behavioral cartography of timed automata
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Robustness of time Petri nets under guard enlargement
• Merge and conquer: state merging in parametric timed automata
• Robustness in timed automata
• Integer Parameter Synthesis for Timed Automata
• Formal Modeling and Analysis of Timed Systems

Cited In (5)

• Synthesis of timing parameters satisfying safety properties
• Distributed parametric model checking timed automata under non-zenoness assumption
• PSyHCoS
• Integer-complete synthesis for bounded parametric timed automata
• Verification and parameter synthesis for real-time programs using refinement of trace abstraction

Uses Software

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

This page was built for publication: Parameter synthesis for hierarchical concurrent real-time systems

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