Comparison of SPIN and VIS for protocol verification |
| |
| Authors: | Hong Peng Sofiène Tahar Ferhat Khendek |
| |
| Affiliation: | (1) Dept. of Electrical & Computer Engineering, Concordia University, 1455 de Maisonneuve W., Montreal, Quebec H3G 1M8, Canada; E-mail: {pengh,tahar,khendek}@ece.concordia.ca, CA |
| |
| Abstract: | In this paper, we compare and contrast SPIN and VIS, two widely used formal verification tools. In particular, we devote special attention to the efficiency of these tools for the verification of communications protocols that can be implemented either in software or hardware. As a basis of our comparison, we formally describe and verify the Asynchronous Transfer Mode Ring (ATMR) medium access protocol using SPIN and its hardware model using VIS. We believe that this study is of particular interest as more and more protocols, like ATM protocols, are implemented in hardware to match high-speed requirements. Published online: 1 March 2002 |
| |
| Keywords: | : SPIN – VIS – Model checking – Formal verification – Protocols |
| 本文献已被 SpringerLink 等数据库收录！ |
|
