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

Data flow anomaly analysis based on model checking

作　　者：陈涛[1,2,3] 许金超[1,2] 钮俊[1,2] 

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

出　　处：《计算机工程与应用》2011年第25期1-4,共4页Computer Engineering and Applications

基　　金：国家自然科学基金(No.90718015);国家高技术研究发展计划(863)(No.2007AA01Z425;No.2009AA012201);国家重点基础研究发展规划(973)(No.2007CB316502);NSFC-微软亚洲研究院联合资助项目(No.60970155);教育部博士点基金项目(No.20090072110035);上海市优秀学科带头人计划项目(No.10XD1404400);高效能服务器和存储技术国家重点实验室开放基金项目(No.2009HSSA06);安徽省自然科学基金(No.11040606M151)~~

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

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

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]