The invention discloses a network service interbehavior formal modeling and deadlock locating method which is used for classifying the existing rules, expanding various classifications and building non-existing rules so as to enable a transformational rule database to be adaptable to a quickly developed formal description language. The existing modeling tool needs manual participation and cannot automatically model, a whole modeling process is invisible to users, and the users cannot determine abnormal locations if the process has error. The method comprises steps of utilizing the expanded or built transformational rule database to automatically model the network service interbehavior which is described by the formal description language; selecting typical cases to verify the build model; and proving the model accuracy and the transformational rule accuracy. A forward searching method is adopted to reproduce and locate abnormal links, so that full-automatic modeling, verifying and locating are realized.