基于模型的持续验证系统
在模型驱动软件开发过程中,基于模型的测试方法往往用于检验软件代码针对软件模型的一致性以确保软件质量.然而,随着当今软件系统规模的不断增大,相应的软件开发过程也变得越来越灵活,代码有时会先于模型被修改,更忠实地体现系统功能和实现机制.传统的基于模型的测试方法只能检测代码之于模型的一致性而不能反作用于模型层面,模型的修改者只能人为地评估修改的正确性,大大降低了效率并增加了系统的潜在隐患.为此,本文对传统基于模型的测试方法的一致性检验进行了扩展,实现了持续验证系统Eunomia,通过从实现系统中抽取表达模型与代码的不一致的性质来自动定位模型中与实际运行系统不匹配的属性,并将其表示为可直接用于模型检测的线性时序逻辑(LTL)表达式,通过不断扩充该LTL属性表达式持续的验证模型与代码间的双向一致性.研究结果表明,Eunomia能有效查找软件模型和代码间的不一致并生成可直接检测模型的系统性质,从而实现了自动化的模型与代码间的双向一致性检测,不仅提高了一致性检测的有效性而且大大减少了人力开销.
软件测试 验证系统 一致性检验 线性时序逻辑表达式
范玲玲 陈森 管映臻
华东师范大学计算机科学技术系,上海200241
国内会议
上海
中文
282-284
2016-04-01（万方平台首次上网日期，不代表论文的发表时间）