Model-checking timed automata with deadlines with Uppaal

DOI10.1007/s00165-011-0185-4zbMath1259.68126OpenAlexW2056343052MaRDI QIDQ1941900

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

real-time systemsmodel-checkingtimed automata with deadlinesurgent actions

Mathematics Subject Classification ID

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

Uses Software

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

Cites Work

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