Abstract
The tool allows verification of communication compatibility of behavior protocols in the form of EBP, a new language for behavior description. The implementation is based on transformation of the input specification into Promela, which is the input language of the Spin model checker.