Using SPIN to Analyse the Tree Identification Phase of the IEEE 1394 High-Performance Serial Bus (FireWire) Protocol |
| |
| Authors: | M Calder A Miller |
| |
| Affiliation: | (1) Department of Computing Science, University of Glasgow, Glasgow, UK, GB |
| |
| Abstract: | We describe how the tree identification phase of the IEEE 1394 high-performance serial bus (FireWire) protocol is modelled
in Promela and verified using SPIN. The verification of arbitrary system configurations is discussed.
Received July 2001/Accepted in revised form November 2002
Correspondence and offprint requests to: Alice Miller, Department of Computing Science, University of Glasgow, 17 Lilybank Gardens, Glasgow G12 8QQ, UK. Email: alice@dcs.gla.ac.uk |
| |
| Keywords: | : Formal verification Model checking SPIN |
| 本文献已被 SpringerLink 等数据库收录！ |
|
