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

计算机工程与应用 ›› 2011, Vol. 47 ›› Issue (25): 1-4.

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

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

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

收稿日期:1900-01-01 修回日期:1900-01-01 出版日期:2011-09-01 发布日期:2011-09-01

Data flow anomaly analysis based on model checking

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

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

摘要/Abstract

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

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

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

陈涛1，2，3，许金超1，2，钮俊1，2. 基于模型检测的数据流异常测试技术研究[J]. 计算机工程与应用, 2011, 47(25): 1-4.

CHEN Tao1，2，3，XU Jinchao1，2，NIU Jun1，2. Data flow anomaly analysis based on model checking[J]. Computer Engineering and Applications, 2011, 47(25): 1-4.

[1]	谭莉娟，郑巍，刘友林，樊鑫，杨丰玉. 面向适航标准的机载软件测试验证方法综述[J]. 计算机工程与应用, 2021, 57(15): 9-22.
[2]	刘友林，郑巍，谭莉娟，樊鑫，杨丰玉. 面向适航标准的机载软件测试验证工具综述[J]. 计算机工程与应用, 2021, 57(11): 1-10.
[3]	王莹. 具有不确定需求的软件测试用例生成方法研究[J]. 计算机工程与应用, 2018, 54(20): 35-41.
[4]	李茜1，王峥1，马建芬1，李娜2. 轻量级移动支付协议公平性分析[J]. 计算机工程与应用, 2018, 54(19): 82-87.
[5]	薛猛，姜淑娟，王荣存. 基于智能优化算法的测试数据生成综述[J]. 计算机工程与应用, 2018, 54(17): 16-23.
[6]	孟令冲1，舒坚2，黄勤涛2，曹伟芳2. 基于SysML活动图的测试序列集约简方法[J]. 计算机工程与应用, 2018, 54(13): 266-270.
[7]	李前利，江华. 命题μ-演算局部模型检测高效算法设计[J]. 计算机工程与应用, 2017, 53(9): 51-56.
[8]	何海江. 基于线性分类算法的软件错误定位模型[J]. 计算机工程与应用, 2017, 53(21): 42-48.
[9]	秦嫚蔓，王峥，王莉. 基于SPIN的远程证明协议的形式化分析及改进[J]. 计算机工程与应用, 2017, 53(1): 34-38.
[10]	王馨樱1，蒋夏军2. 基于UML活动图及混合遗传算法的测试场景生成[J]. 计算机工程与应用, 2017, 53(1): 57-62.
[11]	张柯，张德平. 基于基因表达式编程的错误定位方法[J]. 计算机工程与应用, 2016, 52(9): 6-11.
[12]	吕江华1，刘志锋1，徐亚涛2，周从华1. 基于属性的访问控制策略的正确性验证[J]. 计算机工程与应用, 2016, 52(18): 98-103.
[13]	夏春蕊1，王瑞1，李晓娟1，关永1，张杰2，魏洪兴3. 动态环境下基于概率模型检测的路径规划方法[J]. 计算机工程与应用, 2016, 52(12): 5-11.
[14]	黄延凯，周宇，魏欧. 新型属性图文法反应式规约验证方法[J]. 计算机工程与应用, 2016, 52(12): 15-18.
[15]	王铭1，王瑞1，李晓娟1，关永1，张杰2，魏洪兴3. 非确定性环境中移动机器人避障策略的验证 ——基于形式化建模和概率分析[J]. 计算机工程与应用, 2016, 52(10): 31-38.