基于SPARDL的模型和程序一致性测试.pdf

第30卷第3期
计算机应用研究
ol.30 NG
2013年3月
Application Research of Computers
Mar.2013
基于 SPARDL的模型和程序一致性测试
陈玉祥,浦戈光,禁艳霞,陈铭松',主政',陈朝,顾斌
(1.华东师范大学软件学院,上海20002:;2.北京控制工程研究所,北京100080
摘要:针对周期控制系统的时序一致性进行研究,提出基于 SPARDL( space aircraft description language)的模
型和程序一致性测试方法,通过模型抽取获取模式迁移图和控制流程图,通过程序插桩获取程序执行路径,实现
了自动检測周期控制系统中的模式迁移和模块调用的一致性,給出了基于模式迁移图和控制流程图的覆盖检测
并用于指导程序测试用例的生成。结合具体的周期控制系统,验证了一致性测试方法在实际工程中的有效性。
关键词:时序一致性; SPARD;一致性测试;接受检測;覆盖检测
中图分类号:TP311
文献标志码:A
文章编号:1001-3695(2013)03-0787-05
doi:10.3969/j.issn.1001-3695.2013.03.037
SPARDL, based model-code conformance testing
CHEN Yu-xiang PU G-guang, QI Yan-xia, CHEN Ming-song, WANG Zheny, CHEN Chao-hui, GU Bi
(1. chool of fiare Engineering. st China ormal Uni rsi, Shangha 200 2. hin 2. Reijing Instite of ontrol Engineering, ei-
iing 100080, China
Abstract Focusing on Temporal conformance of periodie c ntrol systems, Lhis paper proposcd a Icsling mcthod bascd on SP
ARDL for model-code conformance testing. It generated the mode diagram and ontrol flow graph by mode extraction, and pro-
dueed Ihe program exccution Irates by program inl rumen l ion. I also presented a al orilhm lo aulomalieally check Ih nsi-
tency about mode transition and module calling inperiodic control systems. And it presented another algorithm to do coverage
specificperiodic control system by the proposed approch and it shows the effectiveness of this approach in indus( '*cle about a
checking based on mode diagram and control flow graph and guide test case generation. Finally, it checked acasest
Key words: Icmporal conformance; space airerall deseription language; conformance lesting; acceptance che king: covera
checking
在软件开发的生命周期中,测试是?个非常重要的阶段。控制系统的需求建模语言,儿其适用」基」模式的、有着混合
做性测试作为一种功能性测试被广泛用于软件测试过程的(迕续的/离散的)状态、有限的周期行为利通信特的制
中。一致性测试是指检测钦件产品的实现是否满足规范的要系统。在每个周期中,系统都会并且只会精确地处在一个模式
求2。在国内外研究中,协议一致性测试是?致性测试研究下,它可以停留在这个模式,或者根据它现在的状态转换到
中最常见的一种,主要川于檢测协议实规与协议规范是否
模式
敛。对丁实时系统的一致性测试也有相关研究,主要方法
周期制系究是一种不会終止的反应式系统( reac: live svs
就是用时间自动机来描述实时系统,用输人/输出流来描述实ten),这种系统按照给定的时间反复执行计算任务。周期控制
时系统需要满足的规范,然后检测输入/输出在时问关系上是系统的时予性不关重要,容易出错只不易检测,因此保证周期
满足一敛性4。现有的模型检测τ具在对大中型系统作ー控制系统的时序性儿为重要。山于系统的非终止性,山.程师
徴性测试付存在状态空问爆炸的瓶预。近年来,基丁模型手动地去檢查时序性费时费力日容易出错。对于周期控制系
的软件测试技术得到了快速的发根。基于模利的测试是?个统的时序性,模式迁移的时序致性关系和模块调用的时序
轻量级的、形式化的验述软件系统的方法?。计对测试任致性关系是控制工程师关注的两个主要时序关系,本文提出了
务,通过对软件功能和结构进行拙象并用易于解的方式进行描
种棊于 SPARDL的模型和程序一致性测试川于对周期控制
述,获得测试模,然后通过檢测算法进行檢测,从而在软件生系统的时序性进行自动檢测。
命周期的早期检测出需求中可能存在的题,但是基于模型的
SPARDL
测试并不能保证模型和程序的·致性。文献[10]针对Java程
序提出了基于UM.活动图的測试用例生成,对UMI.活动图和
SPARDI.作为周期控制系统的建模语分为三个层次:顶
Java程的·致性也进行了测试。随着计算机技术的快速发层展示各个模式及模式辽移关系;中回层描述每个模式的控制
機,计算机软件在嵌入式周期控制系统中发挥着越来越重姴的流程;底层是具体的控制算法。层次结构既反映了嵌入式周期
作用。为了方便软件工程师建煐与分析,木文采用形式化建模控制系统本身的特征,也有利」软件工程师理解开发需求,分
语言 SPARDL为周期性控制系统建模。 SPARDL是一种用
解开发任务1。
收稿日期:2012-07-07;修回日期:2012-09-04基金项目:国家自然科学基金黃助项月(90818024)
作者简介:陈玉祥,男,硕士,主要研究方向为程序分析与验证(chyx6i:hotmail.com);蒲戈光、男,教授,博导,主要研究方向为程序分祈与验
证;漆艳霞,女,工程师,主要研究方向嵌入式软件开发;陈铭松,男,教投,主要研究方向汋软件分析与测试、形式化验证;玉政,男,博士,主要
究方向为模型检测、形式化验迁;陈朝晖,男,工程师,主要研究方向为入式软件开发;顾斌,男,研究页,主要研究方向为嵌入式软件开发