research-article

Open access

The Tree Identify Protocol of IEEE 1394 in μCRL

Authors:

Carron Shankland,

Mark van der ZwaagAuthors Info & Claims

Formal Aspects of Computing, Volume 10, Issue 5

Pages 509 - 531

https://doi.org/10.1007/s001650050030

Published: 01 May 1998 Publication History

PDF eReader

Abstract.

We specify the tree identify protocol of the IEEE 1394 high performance serial multimedia bus at three different levels of detail using μCRL. We use the cones and foci verification technique of Groote and Springintveld to show that the descriptions are equivalent under branching bisimulation, thereby demonstrating that the protocol behaves as expected.

Cited By

View all

Garavel HLuttik B(2024)Four Formal Models of IEEE 1394 Link LayerElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.399.5399(21-100)Online publication date: 27-Mar-2024
https://doi.org/10.4204/EPTCS.399.5
van Spaendonck P(2023)Verification of the Busy-Forbidden ProtocolFundamentals of Software Engineering10.1007/978-3-031-42441-0_10(126-141)Online publication date: 4-May-2023
https://dl.acm.org/doi/10.1007/978-3-031-42441-0_10
Ploeger BSomers LCho YWainwright RHaddad HShin SKoo Y(2007)Analysis and verification of an automatic document feederProceedings of the 2007 ACM symposium on Applied computing10.1145/1244002.1244324(1499-1505)Online publication date: 11-Mar-2007
https://doi.org/10.1145/1244002.1244324
Show More Cited By

Recommendations

Verifying the IEEE 1394 FireWire Tree Identify Protocol with SMV
Abstract.
This case study contains a formal verification of the IEEE 1394 FireWire tree identify protocol. Crucial properties of finite models of the protocol have been validated with state-of-the-art symbolic model checkers. Various optimisation ...
Verification of a sliding window protocol in μCRL and PVS
Abstract
We prove the correctness of a sliding window protocol with an arbitrary finite window size n and sequence numbers modulo 2n. The correctness consists of showing that the sliding window protocol is branching bisimilar to a queue of capacity 2n. The ...
The tree identify protocol of IEEE 1394 in $\mu$CRL

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Formal Aspects of Computing Volume 10, Issue 5

May 1998

141 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 May 1998

Published in FAC Volume 10, Issue 5

Author Tag

Keywords: Process algebra; Verification of distributed systems; Leader election protocols

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

18
Total Citations
View Citations
56
Total Downloads

Downloads (Last 12 months)35
Downloads (Last 6 weeks)8

Reflects downloads up to 07 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Garavel HLuttik B(2024)Four Formal Models of IEEE 1394 Link LayerElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.399.5399(21-100)Online publication date: 27-Mar-2024
https://doi.org/10.4204/EPTCS.399.5
van Spaendonck P(2023)Verification of the Busy-Forbidden ProtocolFundamentals of Software Engineering10.1007/978-3-031-42441-0_10(126-141)Online publication date: 4-May-2023
https://dl.acm.org/doi/10.1007/978-3-031-42441-0_10
Ploeger BSomers LCho YWainwright RHaddad HShin SKoo Y(2007)Analysis and verification of an automatic document feederProceedings of the 2007 ACM symposium on Applied computing10.1145/1244002.1244324(1499-1505)Online publication date: 11-Mar-2007
https://doi.org/10.1145/1244002.1244324
Fokkink WPang JDe Pol J(2006)Cones and fociFormal Methods in System Design10.1007/s10703-006-0004-329:1(1-31)Online publication date: 1-Jul-2006
https://dl.acm.org/doi/10.1007/s10703-006-0004-3
Orzan Svan de Pol JValero Espada M(2005)A State Space Distribution Policy Based on Abstract InterpretationElectronic Notes in Theoretical Computer Science10.1016/j.entcs.2004.10.017128:3(35-45)Online publication date: Apr-2005
https://doi.org/10.1016/j.entcs.2004.10.017
Blom SOrzan S(2005)A distributed algorithm for strong bisimulation reduction of state spacesInternational Journal on Software Tools for Technology Transfer10.1007/s10009-004-0159-47:1(74-86)Online publication date: 25-Jan-2005
https://doi.org/10.1007/s10009-004-0159-4
Luttik B(2003)On the expressiveness of choice quantificationAnnals of Pure and Applied Logic10.1016/S0168-0072(02)00082-9121:1(39-87)Online publication date: May-2003
https://doi.org/10.1016/S0168-0072(02)00082-9
Romijn J(2003)False Loop Detection in the IEEE 1394 Tree Identify PhaseFormal Aspects of Computing10.1007/s00165030000814:3(319-327)Online publication date: Apr-2003
https://doi.org/10.1007/s001650300008
Maharaj SRomijn JShankland C(2003)IEEE 1394 Tree Identify Protocol: Introduction to the Case StudyFormal Aspects of Computing10.1007/s00165030000114:3(200-214)Online publication date: Apr-2003
https://doi.org/10.1007/s001650300001
Fokkink WPang J(2003)Cones and Foci for Protocol Verification RevisitedFoundations of Software Science and Computation Structures10.1007/3-540-36576-1_17(267-281)Online publication date: 28-Feb-2003
https://doi.org/10.1007/3-540-36576-1_17
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract.

Cited By

Recommendations

Verifying the IEEE 1394 FireWire Tree Identify Protocol with SMV

Verification of a sliding window protocol in μCRL and PVS

The tree identify protocol of IEEE 1394 in $\mu$CRL

Comments

Information

Published In

Publisher

Publication History

Author Tag

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations