Premium
Formal Validation of a High Performance Error Control Protocol Using SPIN
Author(s) -
Chan Toong Shoon,
Gorton Ian
Publication year - 1996
Publication title -
software: practice and experience
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.437
H-Index - 70
eISSN - 1097-024X
pISSN - 0038-0644
DOI - 10.1002/(sici)1097-024x(199601)26:1<105::aid-spe3>3.0.co;2-#
Subject(s) - protocol (science) , computer science , reliability engineering , engineering , medicine , pathology , alternative medicine
This paper presents the specification and validation of a high performance error control protocol. A formal specification model of the protocol was described using the PROMELA language. Formal analysis of the protocol model was validated using the SPIN validation tool. The uncovering of several subtle properties of the protocol has demonstrated the advantage of employing formal validation methods in designing distributed systems.