ISSN 1000-1239 CN 11-1777/TP

• 软件技术 •

### 分布式软件系统交互行为建模、验证与测试

1. 1(西安电子科技大学计算理论与技术研究所 西安 710071); 2(西安电子科技大学计算机学院 西安 710071) (zhangc@xidian.edu.cn)
• 出版日期: 2015-07-01
• 基金资助:
基金项目：国家自然科学基金项目(61420106004,61322202,61303031,61272117,61133001,61172147);中央高校基本科研业务费专项资金项目(K5051303005).

### Modeling, Verification and Test of Interactive Behaviors in Distributed Software Systems

Zhang Chen1,2, Duan Zhenhua1,2, Tian Cong1,2, Yu Bin2

1. 1(Institute of Computing Theory and Technology, Xidian University, Xi’an 710071);2(School of Computer Science and Technology, Xidian University, Xi’an 710071)
• Online: 2015-07-01

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.