Model-checking timed automata with deadlines with Uppaal

DOI10.1007/S00165-011-0185-4MaRDI QIDQ1941900zbMATH OpenOpenAlexFDO

Authors Rodolfo Gomez

Publication date 22 March 2013

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

Full work available at URL https://doi.org/10.1007/s00165-011-0185-4

zbMATH Keywords

model-checkingreal-time systemstimed automata with deadlinesurgent actions

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A compositional translation of timed automata with deadlines to Uppaal timed automata
• Symbolic and compositional reachability for timed automata
• Verified model checking of timed automata
• scientific article; zbMATH DE number 1507209
• scientific article; zbMATH DE number 2102690

Cites work

• A theory of timed automata
• Analysis of a biphase mark protocol with Uppaal and PVS
• Analysis of timed systems using time-abstracting bisimulations
• Automatic verification of a lip-synchronisation protocol using UPPAAL
• Compositional specification of timed systems
• Concurrency theory. Calculi and automata for modelling untimed and timed cocurrent systems.
• Formal design and analysis of a gear controller
• Formal Methods for the Design of Real-Time Systems
• Formal Methods for the Design of Real-Time Systems
• Kronos: A verification tool for real-time systems
• Results on the propositional \(\mu\)-calculus
• Symbolic model checking for real-time systems
• The power of reachability testing for timed automata
• Timed automata with urgent transitions

Cited in

(7)

• Temporal reasoning through automatic translation of tock-CSP into timed automata
• Verification of the legOS scheduler using Uppaal
• Parametric Deadlock-Freeness Checking Timed Automata
• Symbolic and compositional reachability for timed automata
• A compositional translation of timed automata with deadlines to Uppaal timed automata
• Formal Methods for the Design of Real-Time Systems
• scientific article; zbMATH DE number 7333236 (Why is no real title available?)

Describes a project that uses

Uses Software

• Uppaal
• Kronos
• MOTOR
• IF-2.0
• MoDeST

This page was built for publication: Model-checking timed automata with deadlines with Uppaal

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