The interoperability of IEC61850intelligent electronic devices（IEDs）is the key to the implementation of IEC61850.In order to solve the problem that it is costly and far between to verify the interoperability of the IEDs produced，an IED interoperability specifying and verifying method based on the formal behavior tree（BT）is put forward for this purpose in their design stage.The external behavioral characteristics of IEDs and the interaction model for the distributed function in interoperation systems are modeled first in the graphical behavior tree mode.Then the BT model is translated into a communicating sequential process（CSP）model，followed by verification of the deadlock and reachability of the interaction model using the process analyzing toolkit（PAT）.By taking the substation timing protection and overcurrent protection interaction model of IEDs as an example for modeling and verifying，the results show that this method can effectively detect the interactive defects in the design of IEDs.