Mechanical verification of the IEEE 1394a root contention protocol using Uppaal2k

DOI10.1007/S100090100059zbMath1053.68580OpenAlexW1575144383WikidataQ126579016 ScholiaQ126579016MaRDI QIDQ5953461

David P. L. Simons, Mariëlle I. A. Stoelinga

Publication date: 2001

Published in: International Journal on Software Tools for Technology Transfer. STTT (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/2066/18891

zbMATH Keywords

model checkingleader election algorithms

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (6)

Symbolic model checking for probabilistic timed automata ⋮ Performance analysis of probabilistic timed automata using digital clocks ⋮ Schedulability of asynchronous real-time concurrent objects ⋮ Compositional schedulability analysis of real-time actor-based systems ⋮ Design and Verification of Fault-Tolerant Components ⋮ Linear parametric model checking of timed automata

Uses Software

• Unnamed Item
• Unnamed Item
• HyTech
• Uppaal

This page was built for publication: Mechanical verification of the IEEE 1394a root contention protocol using Uppaal2k