Premium
An improved protocol reachability analysis technique
Author(s) -
Holzmann Gerard J.
Publication year - 1988
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/spe.4380180203
Subject(s) - reachability , computer science , trace (psycholinguistics) , finite state machine , protocol (science) , state (computer science) , state space , model checking , theoretical computer science , distributed computing , algorithm , mathematics , medicine , linguistics , philosophy , statistics , alternative medicine , pathology
An automated analysis of all reachable states in a distributed system can be used to trace obscure logical errors that would be very hard to find manually. This type of validation is traditionally performed by the symbolic execution of a finite state machine (FSM) model of the system studied. The application of this method to systems of a practical size, though, is complicated by time and space requirements. If a system is larger, more space is needed to store the state descriptions and more time is needed to compare and analyze these states. This paper shows that if the FSM model is abandoned and replaced by a state vector model significant gains in performance are feasible, for the first time making it possible to perform effective validations of large systems.