Abstract: To ensure the correctness of interactive behaviors in distributed software systems, an abstraction approach of modular interaction is proposed. First, system state machine diagrams and object state machine diagrams are utilized to describe state transitions while UML2.0 sequence diagrams are adopted to express the interactive behaviors. Further, the model checking approach with propositional projection temporal logic (PPTL) is applied to verify whether the interactive modular can satisfy the system properties. Using the algorithms, object state machine diagram is transformed into Promela model, and the desired property of the system is specified by a PPTL formula. As a property specification language, PPTL has the expressive power of both full regular and omega regular expressions. At the same time, it is proper for the specification of state sensitive properties. Within the model checker based on Spin, if the system cannot satisfy the property, a counter-example and the execution path can be found. Finally, a novel framework for testing distributed software is given. Based on the verified sequence diagram, test case generation method can be used to get the set of test cases. Experimental results show that the proposed method is useful in improving the effectiveness and reliability of interactive behaviors in distributed software systems.