In IEC 61850， functions of substation intelligent electronic devices（IEDs） can be divided into several logic nodes in order to achieve the purpose of information exchange. There are complex interactive relationships among IEDs and their internal logic nodes（LNs）. How to design and implement this kind of complex behaviors is a key for application of IEC 61850. Formal method may provide a good way. The rigorous description and automatic verification with process algebra for the interaction functions and system behaviors among IEDs and the internal LNs of IEDs are put forward in order to guarantee correction of distribute functions. The IEDs interaction model based on IEC 61850 for time over-current protection is established and the interaction functions and system behaviors are described with Timed communicating sequential processes（CSP）， then automatic verification is done on process analysis toolkit（PAT） platform. Test results show that the method proposed can effectively detect potential defects in specification so as to guide the design of interactive systems of IEDs and save development costs.