Computer Engineering and Applications ›› 2011, Vol. 47 ›› Issue (25): 1-4.

• 博士论坛 • Previous Articles     Next Articles

Data flow anomaly analysis based on model checking

CHEN Tao1,2,3,XU Jinchao1,2,NIU Jun1,2   

  1. 1.Department of Computer Science and Engineering,Tongji University,Shanghai 201804,China
    2.Tongji Branch,National Engineering & Technology Center of High Performance Computer,Shanghai 201804,China
    3.Department of Computer Science and Engineering,Anhui University of Finance & Economics,Bengbu,Anhui 233030,China
  • Received:1900-01-01 Revised:1900-01-01 Online:2011-09-01 Published:2011-09-01

基于模型检测的数据流异常测试技术研究

陈 涛1,2,3,许金超1,2,钮 俊1,2   

  1. 1.同济大学 计算机科学与技术系,上海 201804
    2.国家高性能计算机工程技术中心 同济分中心,上海 201804
    3.安徽财经大学 计算机科学与技术系,安徽 蚌埠 233030

Abstract: The execution of program embodies flows of data in variable.A novel method is proposed to detect data flow anomaly including variable undefined or defined but not referenced or multi-used.The trust pattern of program is defined and program is translated into finite state machine.Based on ALCCTL temporal logic and model checking,verification model satisfies the trust pattern defined.Experiment shows that this method is effective and has been implemented in a defect-oriented testing system.

Key words: variable referenced, software testing, data flow anomaly, model checking

摘要: 程序的执行体现为数据在变量中的流动。对C/C++源代码中变量定义使用情况进行分析,针对变量未赋值就使用、变量重复赋值和变量定义后未使用三种数据流异常情况,使用程序阅读自动机,把程序转换为变量状态机,使用ALCCTL时序逻辑和模型检验工具,验证程序是否满足定义的可信模式。提出了新的静态查找变量使用故障的方法。该方法已应用于面向故障的软件测试系统中。

关键词: 变量使用, 软件测试, 数据流异常, 模型检测