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

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.