• 中国精品科技期刊
  • CCF推荐A类中文期刊
  • 计算领域高质量科技期刊T1类
高级检索

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

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

张琛, 段振华, 田聪, 鱼滨. 分布式软件系统交互行为建模、验证与测试[J]. 计算机研究与发展, 2015, 52(7): 1604-1619. DOI: 10.7544/issn1000-1239.2015.20140244
引用本文: 张琛, 段振华, 田聪, 鱼滨. 分布式软件系统交互行为建模、验证与测试[J]. 计算机研究与发展, 2015, 52(7): 1604-1619. DOI: 10.7544/issn1000-1239.2015.20140244
Zhang Chen, Duan Zhenhua, Tian Cong, Yu Bin. Modeling, Verification and Test of Interactive Behaviors in Distributed Software Systems[J]. Journal of Computer Research and Development, 2015, 52(7): 1604-1619. DOI: 10.7544/issn1000-1239.2015.20140244
Citation: Zhang Chen, Duan Zhenhua, Tian Cong, Yu Bin. Modeling, Verification and Test of Interactive Behaviors in Distributed Software Systems[J]. Journal of Computer Research and Development, 2015, 52(7): 1604-1619. DOI: 10.7544/issn1000-1239.2015.20140244
张琛, 段振华, 田聪, 鱼滨. 分布式软件系统交互行为建模、验证与测试[J]. 计算机研究与发展, 2015, 52(7): 1604-1619. CSTR: 32373.14.issn1000-1239.2015.20140244
引用本文: 张琛, 段振华, 田聪, 鱼滨. 分布式软件系统交互行为建模、验证与测试[J]. 计算机研究与发展, 2015, 52(7): 1604-1619. CSTR: 32373.14.issn1000-1239.2015.20140244
Zhang Chen, Duan Zhenhua, Tian Cong, Yu Bin. Modeling, Verification and Test of Interactive Behaviors in Distributed Software Systems[J]. Journal of Computer Research and Development, 2015, 52(7): 1604-1619. CSTR: 32373.14.issn1000-1239.2015.20140244
Citation: Zhang Chen, Duan Zhenhua, Tian Cong, Yu Bin. Modeling, Verification and Test of Interactive Behaviors in Distributed Software Systems[J]. Journal of Computer Research and Development, 2015, 52(7): 1604-1619. CSTR: 32373.14.issn1000-1239.2015.20140244

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

基金项目: 国家自然科学基金项目(61420106004,61322202,61303031,61272117,61133001,61172147);中央高校基本科研业务费专项资金项目(K5051303005).
详细信息
  • 中图分类号: TP311

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

  • 摘要: 为了确保分析与设计阶段分布式软件系统中模块之间交互行为的正确性,提出了一种分布式软件系统模块交互的抽象方法,分别通过系统状态机图和对象状态机图对各模块状态变迁进行建模,使用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.
计量
  • 文章访问数:  1338
  • HTML全文浏览量:  0
  • PDF下载量:  734
  • 被引次数: 0
出版历程
  • 发布日期:  2015-06-30

目录

    /

    返回文章
    返回