ISSN 1000-1239 CN 11-1777/TP

计算机研究与发展 ›› 2015, Vol. 52 ›› Issue (7): 1604-1619.doi: 10.7544/issn1000-1239.2015.20140244

• 软件技术 • 上一篇    下一篇

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

张琛1,2,段振华1,2, 田聪1,2,鱼滨2   

  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

摘要: 为了确保分析与设计阶段分布式软件系统中模块之间交互行为的正确性,提出了一种分布式软件系统模块交互的抽象方法,分别通过系统状态机图和对象状态机图对各模块状态变迁进行建模,使用UML2.0序列图对模块之间交互行为进行描述.采用基于命题投影时序逻辑的模型检测技术,将对象状态机图转换为Promela模型,系统交互性质转换为命题投影时序逻辑公式,通过模型检测器验证交互模型是否满足于系统的性质,若不满足于该性质,则能够获得反例执行的路径.给出了一个分布式软件系统测试框架,在验证后的序列图模型基础上,使用基于模型的测试用例自动生成方法得到测试用例集合,该集合能够实现对交互行为的有效测试.实例结果表明,该方法可以提高分布式软件系统中模块交互行为的有效性和可靠性.

关键词: 分布式软件系统, 建模, 模型检测, 验证, 测试用例

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.

Key words: distributed software systems, modeling, model checking, verification, test cases

中图分类号: