FORMAL VALIDATION OF A HIGH-PERFORMANCE ERROR CONTROL PROTOCOL USING SPIN

Authors
CHAN TS GORTON I
Citation
Ts. Chan et I. Gorton, FORMAL VALIDATION OF A HIGH-PERFORMANCE ERROR CONTROL PROTOCOL USING SPIN, Software, practice & experience, 26(1), 1996, pp. 105-124
Citations number
20
Categorie Soggetti
Computer Sciences","Computer Science Software Graphycs Programming
Journal title
Software, practice & experience → ACNP
ISSN journal
00380644
Volume
26
Issue
1
Year of publication
1996
Pages
105 - 124
Database
ISI
SICI code
0038-0644(1996)26:1<105:FVOAHE>2.0.ZU;2-H
Abstract
This paper presents the specification and validation of a high perform ance error control protocol, A formal specification model of the proto col was described using the PROMELA language. Formal analysis of the p rotocol model was validated using the SPIN validation tool. The uncove ring of several subtle properties of the protocol has demonstrated the advantage of employing formal validation methods in designing distrib uted systems.