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

Data flow anomaly analysis based on model checking

程序的执行体现为数据在变量中的流动。对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.