English

应用科学学报 ›› 2006, Vol. 24 ›› Issue (4): 377-381.

• 论文 • 上一篇    下一篇

Z规格说明的测试用例自动生成

朱彬1,2, 缪淮扣2, 王娜3   

  1. 1. 上海第二工业大学计算机与信息学院, 上海 201209;
    2. 上海大学计算机工程与科学学院, 上海 200072;
    3. 上海水产大学爱恩学院, 上海 201300
  • 收稿日期:2005-03-02 修回日期:2005-05-20 出版日期:2006-07-31 发布日期:2006-07-31
  • 作者简介:朱彬,博士生,研究方向:形式化方法、软件测试,E-mail:zhubin@it.sspu.cn;缪淮扣,教授,博导,研究方向:形式化方法、软件工程,E-mail:hkmiao@staff.shu.edu.cn
  • 基金资助:
    国家自然科学基金资助项目(60373072)

Automatic Generation and Evaluation of Test Case Based on Z Specifications

ZHU Bing1,2, MIAO Huai-kou2, WANG Na3   

  1. 1. School of Computer & Information, Shanghai Second Polytechnic University, Shanghai 201209, China;
    2. School of Computer Engineering and Science, Shanghai University, Shanghai 200072;
    3. IEN Institute, Shanghai Fisheries University, Shanghai 201300, China
  • Received:2005-03-02 Revised:2005-05-20 Online:2006-07-31 Published:2006-07-31

PDF

108

被引次数

8

摘要： 软件测试是软件质量保证的重要手段,测试用例的生成是软件测试的关键和难点.文中应用范畴划分测试方法产生测试框架,并引入线性规划模型,通过构造线性规划模型来实例化测试框架,并且较好地解决了测试框架是否可行的判断问题.同时结合票据计算的例子,探讨了从Z规格说明推导出测试用例的过程、方法和技术.

关键词: 范畴划分测试, 线性规划, 测试用例, Z, 形式规格说明

Abstract: Software testing is important in software quality assurance, in which test case is crucial.In this paper, a test frame is produced through category-partition, a linear programming model is constructed using the test frame, and linear programming model is solved to give an example of the test frame.A solution is also given to judge whether a test frame is feasible or not.Finally an example is presented based on invoice computation to illustrate the generation process of the test case from Z specifications, with a detailed discussion on the method used.

Key words: category-partition testing, test case, linear programming model, Z, formalized specification

中图分类号: