Parameter synthesis for hierarchical concurrent real-time systems

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

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• HyTech: A model checker for hybrid systems
• Uppaal in a nutshell
• A theory of timed automata
• On the power of non-observable actions in timed automata
• Formal Methods for the Design of Real-Time Systems
• Lectures on Concurrency and Petri Nets
• Symbolic model checking for real-time systems
• 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
• 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
• 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 (2)

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

Uses Software

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

Recommendations

• Parametric timing analysis for real-time systems 👍 👎
• Robust synthesis for real-time systems 👍 👎
• Algorithm for synthesis of real-time systems under reliability constraints 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎

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)