Parameter synthesis for hierarchical concurrent real-time systems

DOI10.1007/S11241-014-9208-6MaRDI QIDQ488231zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 4089320 (Why is no real title available?)
• scientific article; zbMATH DE number 1304998 (Why is no real title available?)
• scientific article; zbMATH DE number 1337733 (Why is no real title available?)
• scientific article; zbMATH DE number 2059569 (Why is no real title available?)
• scientific article; zbMATH DE number 2080044 (Why is no real title available?)
• scientific article; zbMATH DE number 1487728 (Why is no real title available?)
• scientific article; zbMATH DE number 1796145 (Why is no real title available?)
• scientific article; zbMATH DE number 2086955 (Why is no real title available?)
• scientific article; zbMATH DE number 1903354 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• scientific article; zbMATH DE number 3310089 (Why is no real title available?)
• A theory of timed automata
• AN INVERSE METHOD FOR PARAMETRIC TIMED AUTOMATA
• Behavioral cartography of timed automata
• Bounded Model Checking for Parametric Timed Automata
• Decision problems for lower/upper bound parametric timed automata
• Formal Methods for the Design of Real-Time Systems
• Formal Modeling and Analysis of Timed Systems
• HyTech: A model checker for hybrid systems
• Integer Parameter Synthesis for Timed Automata
• Integrated Formal Methods
• Lectures on Concurrency and Petri Nets
• Linear parametric model checking of timed automata
• Merge and conquer: state merging in parametric timed automata
• On the power of non-observable actions in timed automata
• Parametric model-checking of stopwatch Petri nets
• Parametric real-time reasoning
• Precise robustness analysis of time Petri nets with inhibitor ARCS
• Quantitative robustness analysis of flat timed automata
• Robust reachability in timed automata: a game-based approach
• Robustness in timed automata
• Robustness of time Petri nets under guard enlargement
• Scheduling with timed automata
• Specification and Proof in Real Time CSP
• Symbolic model checking for real-time systems
• The octahedron abstract domain
• Time separation of events: an inverse method
• Timed Automata Can Always Be Made Implementable
• Timed verification of the generic architecture of a memory circuit using parametric timed automata
• Uppaal in a nutshell

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

Describes a project that uses

Uses Software

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

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)