False loop detection in the IEEE 1394 tree identify phase

DOI10.1007/S001650300008MaRDI QIDQ1402479zbMATH OpenOpenAlexFDO

Authors Judi Romijn

Publication date 27 August 2003

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

Full work available at URL https://doi.org/10.1007/s001650300008

zbMATH Keywords

AlgorithmVerificationTimed automataReal-timeSpanning treeDynamic networkLoop detectionProtocol

Mathematics Subject Classification ID

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

Recommendations

• Specification and verification of the tree identify protocol of IEEE 1394 in rewriting logic
• The tree identify protocol of IEEE 1394 in \(\mu\)CRL
• Using SPIN to analyse the tree identification phase of the IEEE 1394 high-performance serial bus (FireWire) protocol
• Verifying the IEEE 1394 fireWire tree identify protocol with SMV
• A mechanically proved and incremental development of IEEE 1394 tree identify protocol
• IEEE 1394 tree identify protocol: Introduction to the case study
• Lock Detection in Phase-Locked Loops
• Mechanical verification of the IEEE 1394a root contention protocol using Uppaal2k
• Verification of the link layer protocol of the IEEE-1394 serial bus (FireWire): An experiment with E-LOTOS

Cited in

(1)

• Using SPIN to analyse the tree identification phase of the IEEE 1394 high-performance serial bus (FireWire) protocol

Describes a project that uses

Uses Software

• Uppaal
• Uppaal2k

This page was built for publication: False loop detection in the IEEE 1394 tree identify phase

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