Valira/Valisyn-Protocol Validator/Synthesizer User's Manual (Version 1.2)

ID
TR-88-19
Authors
Son T. Vuong and T. Lau
Publishing date
January 1988
Abstract
VALIRA (VALidation via Reachability Analysis) is a protocol validation fool that accepts a given protocol specification in a communicating finite state machine (CFSM) model and performs a validation via reachability analysis. The syntactic properties of the protocol, including state ambiguities, state deadlocks, unspecified receptions, non-executable interactions, and unbounded channels, are analyzed and reported.