How to stop time stopping

DOI10.1007/S00165-006-0010-7MaRDI QIDQ855006zbMATH OpenOpenAlexFDO

Authors Howard Bowman, Rodolfo Gomez

Publication date 20 December 2006

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00165-006-0010-7

zbMATH Keywords

Model checkingTimed automataNon-zenoness conditionsZeno-timelocks

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A tool for the syntactic detection of Zeno-timelocks in timed automata
• Efficient Detection of Zeno Runs in Timed Automata
• Coarse abstractions make Zeno behaviours difficult to detect
• Coarse abstractions make Zeno behaviours difficult to detect
• Distributed parametric model checking timed automata under non-zenoness assumption

Cites work

• scientific article; zbMATH DE number 1670779 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 1796156 (Why is no real title available?)
• A theory of timed automata
• A tool for the syntactic detection of Zeno-timelocks in timed automata
• Automated verification of an audio-control protocol using UPPAAL
• Automatic verification of a lip-synchronisation protocol using UPPAAL
• Concurrency theory. Calculi and automata for modelling untimed and timed cocurrent systems.
• Formal Modeling and Analysis of Timed Systems
• Guided synthesis of control programs using UPPAAL
• Kronos: A verification tool for real-time systems
• Lectures on Concurrency and Petri Nets
• Model-checking in dense real-time
• Symbolic model checking for real-time systems
• The power of reachability testing for timed automata

Cited in

(10)

• Coarse abstractions make Zeno behaviours difficult to detect
• Efficient Detection of Zeno Runs in Timed Automata
• Coarse abstractions make Zeno behaviours difficult to detect
• Distributed parametric model checking timed automata under non-zenoness assumption
• Efficient emptiness check for timed Büchi automata
• Static detection of Zeno runs in UPPAAL networks based on synchronization matrices and two data-variable heuristics
• Accelerating worst case execution time analysis of timed automata models with cyclic behaviour
• A compositional translation of timed automata with deadlines to Uppaal timed automata
• A tool for the syntactic detection of Zeno-timelocks in timed automata
• A menagerie of timed automata

Describes a project that uses

Uses Software

• Kronos
• HyTech
• Uppaal

This page was built for publication: How to stop time stopping

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