孫　晶　金曉文

(北方工業(yè)大學(xué)信息工程學(xué)院　北京 100144)

?

模型檢測(cè)引導(dǎo)的TTCN-3測(cè)試套生成技術(shù)研究

孫晶金曉文

(北方工業(yè)大學(xué)信息工程學(xué)院北京 100144)

針對(duì)軟件測(cè)試的不完備性以及軟件測(cè)試自動(dòng)化問(wèn)題，提出在測(cè)試過(guò)程中將模型檢測(cè)前置于傳統(tǒng)測(cè)試，將模型檢測(cè)與測(cè)試相結(jié)合。通過(guò)分析模型檢測(cè)中的形式化規(guī)約明確測(cè)試目的，并轉(zhuǎn)換成TTCN-3(Testing and Test Control Notation) 抽象測(cè)試套。進(jìn)一步利用規(guī)約中本身存在的正例，與數(shù)據(jù)類型描述文件相關(guān)聯(lián)，從而生成測(cè)試用例。分析TTCN-3開(kāi)發(fā)模式，基于標(biāo)簽轉(zhuǎn)換系統(tǒng)與TTCN-3行為樹(shù)的等價(jià)性，提出模型檢測(cè)引導(dǎo)的抽象測(cè)試套生成算法，并實(shí)現(xiàn)TTCN-3抽象測(cè)試套的自動(dòng)生成。

軟件測(cè)試模型檢測(cè)TTCN-3測(cè)試套μ演算

0　引　言

近年來(lái)，模型檢測(cè)以其自動(dòng)化程度高的特點(diǎn)在軟件測(cè)試領(lǐng)域得到了廣泛關(guān)注。由于模型檢測(cè)可以自動(dòng)執(zhí)行，并能在系統(tǒng)不滿足性質(zhì)時(shí)提供反例路徑來(lái)說(shuō)明不滿足的原因，因此在工業(yè)界比演繹證明更受推崇。而測(cè)試是保證軟件產(chǎn)品可靠性和正確性的傳統(tǒng)手段，相較模型檢測(cè)而言自動(dòng)化不高，手動(dòng)選取測(cè)試用例有不完備性。

模型檢測(cè)是關(guān)于自動(dòng)驗(yàn)證并行或者分布式系統(tǒng)性質(zhì)的算法和方法，它的基本思想是用狀態(tài)遷移系統(tǒng)(S)表示系統(tǒng)的行為，用模態(tài)邏輯公式(F)描述系統(tǒng)的性質(zhì)。這樣“系統(tǒng)是否具有所期望的性質(zhì)”就轉(zhuǎn)化為數(shù)學(xué)問(wèn)題“狀態(tài)遷移系統(tǒng)S是否是公式F的一個(gè)模型？”，用公式表示為S╞F[1]。對(duì)有窮狀態(tài)系統(tǒng)，這個(gè)問(wèn)題是可判定的，即可以用計(jì)算機(jī)程序在有限時(shí)間內(nèi)自動(dòng)確定。而基于模型檢測(cè)的測(cè)試用例自動(dòng)生成已經(jīng)有較長(zhǎng)的研究歷程。由P.Ammann[2]等提出的貫徹始終的基本思想是利用模型檢測(cè)工具提供的描述語(yǔ)言刻畫(huà)軟件需要滿足的性質(zhì)，并利用工具進(jìn)行全空間的搜索；當(dāng)性質(zhì)不滿足的時(shí)候，工具會(huì)捕捉所有的反例路徑，然后再根據(jù)反例提供的線索生成測(cè)試用例。Cong Tian[3]等也提出了利用模型檢測(cè)從謂語(yǔ)連詞中自動(dòng)生成測(cè)試用例的方法。并且提出了一個(gè)算法將測(cè)試用例的生成從基于原子謂語(yǔ)表達(dá)式的連接轉(zhuǎn)化為模型檢測(cè)。而韓國(guó)釜慶大學(xué)Jaeyoun Jung[4]等實(shí)現(xiàn)了一種為L(zhǎng)TS過(guò)程規(guī)范而提出的模型檢測(cè)工具，它可以用來(lái)檢查死鎖，活鎖，可達(dá)狀態(tài)以及動(dòng)作。在國(guó)內(nèi)，蘇開(kāi)樂(lè)[5]等提出了一個(gè)關(guān)于時(shí)態(tài)邏輯CTL* 的符號(hào)化模型檢測(cè)算法。 該算法通過(guò)所謂的tableau 構(gòu)造方法來(lái)判定一個(gè)有限狀態(tài)系統(tǒng)是否滿足CTL* 規(guī)范。清華大學(xué)何愷鐸[6]等提出了一種基于謂詞抽象和反例引導(dǎo)抽象求精技術(shù)對(duì)源程序進(jìn)行建模和驗(yàn)證的模型檢測(cè)方法， 并結(jié)合自行研發(fā)的Jchecker 工具詳細(xì)介紹了該軟件模型檢測(cè)技術(shù)的運(yùn)作過(guò)程和關(guān)鍵算法。而與此同時(shí)，TTCN-3作為一種功能強(qiáng)大的基于響應(yīng)系統(tǒng)的黑箱測(cè)試標(biāo)準(zhǔn)，早已發(fā)展成為了一種通用的測(cè)試規(guī)格語(yǔ)言。早在1997年，國(guó)內(nèi)學(xué)者郝瑞兵[7]等就已提出了一種形式化的基于TTCN的測(cè)試執(zhí)行方法。其使用了標(biāo)號(hào)變遷系統(tǒng)(LTS)刻畫(huà)了這一方法的整個(gè)執(zhí)行過(guò)程，并給出了具體實(shí)現(xiàn)。而蔣凡[8]等在經(jīng)過(guò)多年在TTCN-3領(lǐng)域中的研究之后，其概括地提出了TTCN-3 測(cè)試套開(kāi)發(fā)模式并實(shí)現(xiàn)了應(yīng)用。而Niusha Hakimipour[9]等，提出了一個(gè)從“需求”中生成測(cè)試用例的方法，并使用行為樹(shù)(BT)來(lái)建模系統(tǒng)需求。國(guó)防科技大學(xué)顏烔[10]等在基于模型的軟件測(cè)試綜述一文，概述了基于模型的軟件測(cè)試的方法，闡明軟件測(cè)試模型是對(duì)軟件行為和軟件結(jié)構(gòu)的抽象描述，可以用于生成軟件測(cè)試?yán)?/p>

可是不論是新興的模型檢測(cè)還是傳統(tǒng)的軟件測(cè)試都有其弊端，模型檢測(cè)會(huì)由于值域太泛而導(dǎo)致?tīng)顟B(tài)爆炸[11]，而傳統(tǒng)測(cè)試又有其不完備性[12]。所以本文提出一種模型檢測(cè)引導(dǎo)的TTCN-3測(cè)試套生成技術(shù)，該技術(shù)通過(guò)對(duì)將軟件的所有狀態(tài)轉(zhuǎn)化成LTS(Label Transition System)，然后根據(jù)測(cè)試目的對(duì)標(biāo)簽轉(zhuǎn)換系統(tǒng)進(jìn)行形式化規(guī)約，在明確了測(cè)試目的之后進(jìn)行自動(dòng)化的軟件測(cè)試。

1　TTCN-3概述

TTCN是一個(gè)由ETSI(European Telecommunications Standards Institute)維護(hù)的全球適用的標(biāo)準(zhǔn)測(cè)試語(yǔ)言。在第三代標(biāo)準(zhǔn)中，TTCN-3是一個(gè)現(xiàn)代的且靈活的語(yǔ)言，其廣泛的接口機(jī)制，被用于描述許多類型的系統(tǒng)測(cè)試。典型的應(yīng)用領(lǐng)域?yàn)橄到y(tǒng)測(cè)試、交互性測(cè)試、協(xié)議測(cè)試、業(yè)務(wù)測(cè)試、模塊測(cè)試等。

TTCN-3作為標(biāo)準(zhǔn)測(cè)試語(yǔ)言，其不僅囊括了普通程序設(shè)計(jì)語(yǔ)言的簡(jiǎn)單明了，易于人機(jī)交互。而且其擁有便于測(cè)試的功能支持，如動(dòng)態(tài)測(cè)試配置、測(cè)試判決處理、定時(shí)器機(jī)制、通信機(jī)制等。

TTCN-3連接是端口到端口和端口到測(cè)試系統(tǒng)接口的連接。其測(cè)試配置如圖1所示。所以從某一方面而言，TTCN-3所描述的測(cè)試系統(tǒng)就是根據(jù)測(cè)試目的進(jìn)行動(dòng)態(tài)測(cè)試配置，并通過(guò)定時(shí)器機(jī)制、通信機(jī)制等進(jìn)行測(cè)試并最后進(jìn)行測(cè)試判決處理。

圖1　動(dòng)態(tài)測(cè)試配置

用TTCN-3描述測(cè)試系統(tǒng)，就是抽象測(cè)試套的生成。目前的方式還只是限于手動(dòng)編寫(xiě)文本格式的TTCN-3文件，或用GFT圖形化標(biāo)準(zhǔn)進(jìn)行轉(zhuǎn)化。但上述兩種方式是人為的，比較被動(dòng)。由于TTCN-3的層次結(jié)構(gòu)和基本作用域范圍的控制[13]，手動(dòng)書(shū)寫(xiě)TTCN-3測(cè)試套還是存在一定的錯(cuò)誤和風(fēng)險(xiǎn)。

對(duì)于TTCN-3的執(zhí)行環(huán)境，目前在國(guó)內(nèi)外已有研究和應(yīng)用。如Elvior、OpenTTCN Tester、Testing Technologies公司開(kāi)發(fā)的TTworkbench都是TTCN-3官網(wǎng)上公布的很權(quán)威的TTCN-3的編譯、運(yùn)行環(huán)境。而國(guó)內(nèi)， 中國(guó)科學(xué)技術(shù)大學(xué)也已開(kāi)發(fā)了協(xié)議測(cè)試工具——LoongTesting，且兼容了Windows及Linux平臺(tái)。

2　TTCN-3測(cè)試套的自動(dòng)生成

2.1模型檢測(cè)引導(dǎo)

模型檢測(cè)的基本步驟為：建模、規(guī)范和驗(yàn)證。

在建模過(guò)程中，需要對(duì)系統(tǒng)功能進(jìn)行描述，常用的一種描述形式是標(biāo)簽轉(zhuǎn)換系統(tǒng)LTS。規(guī)范是根據(jù)測(cè)試目的(系統(tǒng)期望滿足的性質(zhì))進(jìn)行形式化描述，之后通過(guò)模型檢測(cè)工具進(jìn)行驗(yàn)證。

例如一個(gè)LTS描述的被測(cè)系統(tǒng)，狀態(tài)S={0,1,2}， 初態(tài)I={0}，轉(zhuǎn)移動(dòng)作→={<0,1>, <1,1>*,<1,2>}，活動(dòng)A={a0,a1,a2…,a9}，謂詞P={True,False}。LLTS={, *, }表達(dá)了一個(gè)活動(dòng)a0,a1執(zhí)行的實(shí)例，如圖2所示。對(duì)于系統(tǒng)的某個(gè)功能進(jìn)行描述，即對(duì)標(biāo)簽轉(zhuǎn)換系統(tǒng)的某一個(gè)性質(zhì)進(jìn)行斷言描述，則可描述為：[a0.a1*]true。

圖2　被測(cè)系統(tǒng)的LTS描述

本實(shí)驗(yàn)項(xiàng)目組分為三部分，第一部分是對(duì)軟件行為和軟件結(jié)構(gòu)的抽象描述，將被測(cè)系統(tǒng)用LTS的形式(控制流圖)描述出來(lái)，并轉(zhuǎn)化成為服務(wù)描述語(yǔ)言bpel和wsdl進(jìn)行物理存儲(chǔ). 第二部分涉及測(cè)試目的引導(dǎo)的模型檢測(cè)，即通過(guò)明確測(cè)試目的，轉(zhuǎn)化為模態(tài)邏輯公式μ演算。并與LTS描述的被測(cè)系統(tǒng)相結(jié)合，進(jìn)行模型檢測(cè)。本文是第三部分，通過(guò)分析模型檢測(cè)中的形式化規(guī)約(μ演算)明確測(cè)試目的，自動(dòng)化轉(zhuǎn)換成TTCN-3 抽象測(cè)試套。可以看出，經(jīng)過(guò)本項(xiàng)目組其他工作之后，我們已得到了一個(gè)構(gòu)造完整的測(cè)試模型。

2.2測(cè)試套生成

對(duì)TTCN-3測(cè)試系統(tǒng)而言，針對(duì)特定的被測(cè)系統(tǒng)，用戶自定義部分有兩個(gè)方面：(1) 根據(jù)被測(cè)系統(tǒng)測(cè)試要求編寫(xiě) TTCN-3 測(cè)試?yán)?2) 根據(jù)TTCN-3測(cè)試?yán)捅粶y(cè)系統(tǒng)編寫(xiě)或者重用可執(zhí)行測(cè)試套(適配器)[8]。

對(duì)于黑盒測(cè)試語(yǔ)言TTCN-3而言，首先要明確其測(cè)試目的。在項(xiàng)目組第二部分的工作中，已將形式化規(guī)約描述的活動(dòng)序列轉(zhuǎn)化為μ演算來(lái)描述，這就幫助明確了測(cè)試目的。因?yàn)槠渲幻枋隽岁P(guān)鍵活動(dòng)，為了方便理解，可以將其看做是“簡(jiǎn)化的LTS”。而基于LTS與TTCN-3行為樹(shù)的等價(jià)性[14]，提出了抽象測(cè)試套生成算法。

算法1抽象測(cè)試套生成算法

Input: the μ-calculus

Output: TTCN-3 behavior tree

BEGIN

Read the μ-calculus, extract LTS sequence in the μ-calculus

FOR each LTS sequence DO

IF sequence=a THEN rewrite to s replace True with pass and False with fail.

IF sequence=R1 ″.″ R2, THEN rewrite to {s1, {s2?s1}}

//順序結(jié)構(gòu)

IF sequence= R1 ″|″ R2, THEN rewrite to {{s1?s}, {s2?s}}

//分支結(jié)構(gòu)

IF sequence= R1 ″*″R2, THEN rewrite to {{s1}*,{s2?s1}}

//循環(huán)結(jié)構(gòu)

IF sequence=R1″+″ R2, THEN rewrite to {{s1}+,{s2?s1}}

//至少執(zhí)行一次的循環(huán)結(jié)構(gòu)

END

END

在提出了算法后，就可以將其進(jìn)行自動(dòng)化的轉(zhuǎn)化，實(shí)現(xiàn)可執(zhí)行測(cè)試套的自動(dòng)生成。我們先從左至右掃描μ演算文件，分離存儲(chǔ)事件(event)和邏輯部分(logic)，并解析相關(guān)的bpel文件，根據(jù)μ演算與TTCN-3的映射關(guān)系，依次生成TTCN-3抽象測(cè)試套的主體部分。

do_module();

do_component();

do_function();

do_testcase();

由于μ演算中正則公式的邏輯表達(dá)形如R1.R2、R1|R2、R1*R2、R1+R2， 所以要借用編譯原理的中回溯技術(shù)，來(lái)完成μ演算的掃描與解析，并將μ演算中對(duì)應(yīng)的邏輯部分翻譯成TTCN-3的邏輯表達(dá)。

TTCN-3與μ演算的重要映射關(guān)系如表1所示， 其余未在表中列出的關(guān)系，如測(cè)試套、定時(shí)器、主測(cè)試成分等的名字，采用了自動(dòng)化命名的方式，形如TC_0()。

表1　TTCN-3與μ演算的重要映射關(guān)系

μ演算相同的事件門操作(event)會(huì)抽象成同一組件的行為，會(huì)在同一個(gè)函數(shù)中來(lái)實(shí)現(xiàn)。例如，一個(gè)μ演算是這樣描述一個(gè)系統(tǒng)的["op_1 !Request_1″.″op_1 ?Response_1″]true.系統(tǒng)首先會(huì)產(chǎn)生一個(gè)主測(cè)試成分mtcType,然后根據(jù)對(duì)應(yīng)系統(tǒng)描述會(huì)產(chǎn)生op_1function(),然后在測(cè)試?yán)齮estcase中根據(jù)邏輯生成調(diào)用function的關(guān)系。

又例如，一個(gè)復(fù)雜一些的μ演["op_1 !Request_1″.″op_1 ?Response_1″.″op_2 !Request_2″.″op_2 ?Response_2″]true，則會(huì)對(duì)應(yīng)倆個(gè)函數(shù)function,分別為op_1function() 和op_2function()，測(cè)試套中表現(xiàn)了函數(shù)之間的調(diào)用關(guān)系?？梢钥闯鰧?duì)于上述μ演算樣例而言，邏輯關(guān)系是順序的，且對(duì)應(yīng)描述如下：

testcase TC_0() runs on mtcType{

op_1function();

op_2function();

}

3　測(cè)試?yán)淖詣?dòng)生成

在構(gòu)造完測(cè)試模型之后，我們的任務(wù)就是生成和執(zhí)行測(cè)試?yán)齕10]。由于傳統(tǒng)測(cè)試中的不完備性，對(duì)于測(cè)試?yán)倪x取有局限性。模型檢測(cè)自動(dòng)化全部遍歷所有空間狀態(tài)，可以對(duì)所有的活動(dòng)序列的屬性進(jìn)行形式化規(guī)約，并檢測(cè)出不符合形式化規(guī)約的反例路徑，這就借鑒了傳統(tǒng)的基于模型檢測(cè)的測(cè)試用例自動(dòng)生成的方法，而與此同時(shí)應(yīng)該注意到形式化規(guī)約中，是存在正例路徑的，所以拓展這一部分，并將得到的模型檢測(cè)的結(jié)果與相關(guān)的數(shù)據(jù)類型描述文件(bpel組合中的wsdl)進(jìn)行關(guān)聯(lián)，解析bpel中名稱空間里wsdl的位置(lns)，同時(shí)根據(jù)需要獲取數(shù)據(jù)類型的消息名稱來(lái)提取測(cè)試用例。

例如，一個(gè)μ演算是這樣描述一個(gè)系統(tǒng)[″op_1 !Request_1″.″op_1 ?Response_1″]true. 我們可以通過(guò)這樣的形式化規(guī)約獲得發(fā)送和接受的消息名稱Request_1和Response_1，然后檢索相關(guān)的數(shù)據(jù)類型描述文件，就可以得到一個(gè)精確的測(cè)試用例的類型。具體提取的信息截取如下：

[org.dom4j.Namespace@6f2c2097 [Namespace: prefix mapped to URI ″http://docs.oasis-open.org/wsbpel/2.0/process/executable″], org.dom4j.Namespace@1d3b6455 [Namespace: prefix lns mapped to URI ″C:/Users/Administrator/Desktop/常用文檔/P0/wsdl″]]

Request_1

Retrieving document at ′C:/Users/Administrator/Desktop/常用文檔/P0/wsdl/1.wsdl′.

Service Name:

1

Port Name:

(1)驗(yàn)證了水是TSR反應(yīng)發(fā)生的必要條件，在無(wú)水條件下 ，CaSO4不能引發(fā)TSR反應(yīng)生成H 2 S。

PortType_1

Operation Name:

op_1

Messages:

Request_1

parameter name:i parameter type:integer

可以看出根據(jù)wsdl提取出了變量的數(shù)據(jù)類型，最后依照傳統(tǒng)測(cè)試中等價(jià)類劃分的方法提取測(cè)試用例，嵌入到之前已經(jīng)生成好的抽象測(cè)試套的邏輯框架中。對(duì)于復(fù)雜數(shù)據(jù)類型如record等，提供了數(shù)據(jù)模板模塊，用戶可以根據(jù)測(cè)試需求與模板格式進(jìn)行手動(dòng)加載。

4　案例研究與評(píng)估

4.1案例研究

圖3　八皇后主程序程序流圖

八皇后問(wèn)題是一個(gè)以國(guó)際象棋為背景的問(wèn)題：如何能夠在8×8的國(guó)際象棋棋盤(pán)上放置八個(gè)皇后，使得任何一個(gè)皇后都無(wú)法直接吃掉其他的皇后。為了達(dá)到此目的，任兩個(gè)皇后都不能處于同一條橫行、縱行或斜線上。

如果針對(duì)主程序進(jìn)行完整測(cè)試，則對(duì)應(yīng)μ演算描述為：

[″op_1 !Request_1″.″op_1 ?Response_1″.(″op_2 !Request_2″.″op_2 ?Response_2″.″op_3 !Request_3″.″op_3 ?Response_3″.(″op_4 !Request_4″.″op_4 ?Response_4″.″op_5 !Request_5″.″op_5 ?Response_5″)*.″op_6 !Request_6″.″op_6 ?Response_6″)*.″op_7 !Request_7″.″op_7 ?Response_7″.″op_P1 !Request_P1″.″op_P1 ?Response_P1″]true

通過(guò)分析上述形式化規(guī)約，和前期已經(jīng)生成好的被測(cè)系統(tǒng)的形式化描述文件bpel和wsdl，自動(dòng)生成測(cè)試套。由于測(cè)試套龐大復(fù)雜，在此只列出測(cè)試套的數(shù)據(jù)類型定義如圖4及測(cè)試?yán)鐖D5所示。

圖4　數(shù)據(jù)類型定義　　　　　　　圖5　測(cè)試?yán)?/p>

將生成的測(cè)試套加載在TTCN-3編譯運(yùn)行環(huán)境中進(jìn)行驗(yàn)證，并根據(jù)被測(cè)系統(tǒng)編寫(xiě)配套的編解碼器和適配器。得到運(yùn)行結(jié)果如圖6所示，可以看到定時(shí)器啟用了164次符合邏輯預(yù)期。

4.2評(píng)估

在經(jīng)過(guò)大量的學(xué)習(xí)和助教工作之后，我們發(fā)現(xiàn)手動(dòng)編寫(xiě)TTCN-3測(cè)試套是需要大量的前期投入的，這包括對(duì)于人員的技術(shù)培訓(xùn)、實(shí)驗(yàn)環(huán)境的搭建等等。

圖7　手動(dòng)/自動(dòng)效率對(duì)比圖

在明確測(cè)試目的的前提下，對(duì)手動(dòng)編寫(xiě)TTCN-3測(cè)試套(在保證準(zhǔn)確的情況下)和本文中提到的自動(dòng)生成TTCN-3測(cè)試套(包括配置路徑的時(shí)間)進(jìn)行了效率對(duì)比，如圖7針對(duì)同一源代碼，生成同一測(cè)試套，然后對(duì)比其所用時(shí)間?？梢钥闯鍪謩?dòng)編寫(xiě)測(cè)試套的方法所用的時(shí)間會(huì)隨著被測(cè)系統(tǒng)規(guī)模的增長(zhǎng)呈幾近指數(shù)型增長(zhǎng)，而自動(dòng)生成的時(shí)間增長(zhǎng)并不明顯。

5　結(jié)　語(yǔ)

關(guān)于TTCN-3測(cè)試套自動(dòng)生成以及測(cè)試?yán)傻难芯坑性S多。蘭毓華等人[15]提出了一種基于 Z 規(guī)格說(shuō)明的軟件測(cè)試用例自動(dòng)生成方法， 通過(guò)對(duì)軟件Z規(guī)格說(shuō)明的分析，找出描述軟件輸入、 輸出約束的線性謂詞，經(jīng)過(guò)線性謂詞轉(zhuǎn)換， 線性謂詞到線性不等式組的轉(zhuǎn)換， 找出區(qū)域邊界頂點(diǎn)和邊界附近的測(cè)試點(diǎn)等過(guò)程自動(dòng)生成測(cè)試用例。陳萍等[16]提出了根據(jù) TTCN-3標(biāo)準(zhǔn)的第三部分GFT與TTCN-3核心語(yǔ)言的內(nèi)在關(guān)聯(lián)以及標(biāo)準(zhǔn)中的語(yǔ)法規(guī)定的一種TTCN-3測(cè)試套生成方法，并設(shè)計(jì)開(kāi)發(fā)了一套由圖形表示格式自動(dòng)生成用核心語(yǔ)言描述的測(cè)試套的轉(zhuǎn)換工具。趙玉蘭等[17]介紹一個(gè)在GE-LOTOS的基礎(chǔ)上自動(dòng)產(chǎn)生TTCN測(cè)試套的工具， 該工具是基于由形式描述技術(shù)語(yǔ)言E-LOTOS轉(zhuǎn)換成的GE-LOTOS。 并對(duì) Internet上的一個(gè)標(biāo)準(zhǔn)路由信息協(xié)議(RIP協(xié)議)進(jìn)行了TTCN測(cè)試套的應(yīng)用。

與上述研究工作不同， 我們既不是基于Z規(guī)格說(shuō)明，也不基于圖形。與基于E-LOTOS有異曲同工之妙，都是形式化描述為根基的。本文主要研究模型檢測(cè)引導(dǎo)的TTCN-3測(cè)試套自動(dòng)生成方法。雖然測(cè)試套包含測(cè)試用例選擇內(nèi)容，但本文的重點(diǎn)在測(cè)試邏輯執(zhí)行部分， 而在測(cè)試用例的選擇方面， 采用的是提取模態(tài)邏輯描述中存在的正例，與相關(guān)的數(shù)據(jù)描述文件關(guān)聯(lián)，從而提取測(cè)試用例。本文基于 LTS 到行為樹(shù)轉(zhuǎn)換的理論方法[14]， 提出了模型檢測(cè)引導(dǎo)的TTCN-3抽象測(cè)試套生成算法，并給出了TTCN測(cè)試套自動(dòng)生成的技術(shù)方案，且實(shí)際檢驗(yàn)了該方案的可行性。

本文的不足之處在于只能生成簡(jiǎn)單數(shù)據(jù)類型的測(cè)試用例。但也基本上規(guī)避了顏烔[10]等在基于模型的軟件測(cè)試綜述一文中提到的基于模型的軟件測(cè)試的缺點(diǎn)，即狀態(tài)空間爆炸問(wèn)題。而傳統(tǒng)的手動(dòng)編寫(xiě)TTCN-3測(cè)試套的模式效率不高，本文中提出的自動(dòng)化生成的模式一定程度上提高了測(cè)試套生成的效率。

[1] 林惠民,張文輝.模型檢測(cè):理論、方法與應(yīng)用[J].電子學(xué)報(bào),2002,30(12A):1907-1912.

[2] Ammann P,Black P E,Ding W.Model checkers in software testing[R].Technical Reprot NIST-IR 677,Naltional Institute of Standards and Technology,2002.

[3] Cong Tian,Shaoying Liu,Nakajima S.Utilizing Model Checking for Automatic Test Case Generation from Conjunctions of Predicates[C]//Berlin:Software Testing, Verification and Validation Workshops (ICSTW),2011 IEEE Fourth International Conference on,2011:304-309.

[4] Jaeyoun Jung,Youngeung Kim,Yeondae Chung,et al.A Study on Implementation of Model Checking Tool for Verifying LTS Specifications[C]//Toyko:Information Networking,1998.(ICOIN-12) Proceedings,Twelfth International Conference on,1998:539-543.

[5] 蘇開(kāi)樂(lè),駱翔宇,呂關(guān)鋒.符號(hào)化模型檢測(cè)CTL[J].計(jì)算機(jī)學(xué)報(bào),2005,28(11):1798-1806.

[6] 何愷鐸,顧明,宋曉宇,等.面向源代碼的軟件模型檢測(cè)及其實(shí)現(xiàn)[J].計(jì)算機(jī)科學(xué),2009,36(1):267-272.

[7] 郝瑞兵,吳建平,史美林.一種形式化的基于TTCN的測(cè)試執(zhí)行方法[J].軟件學(xué)報(bào),1997,8(5):367-375.

[8] 劉小勇,蔣凡.TTCN-3測(cè)試套開(kāi)發(fā)模式及其應(yīng)用[J].計(jì)算機(jī)輔助工程,2005,14(2):21-25.

[9] Niusha Hakimipour,Paul Strooper.Exploring an approach to model-based testing from Behavior Trees[C]//Hong Kong:Software Engineering Conference (APSEC),2012 19th Asia-Pacific (Volume:2),2012:80-86.

[10] 顏炯,王戟,陳火旺.基于模型的軟件測(cè)試綜述[J].計(jì)算機(jī)科學(xué),2004,31(2):184-187.

[11] Gerard J Holzmann,Rajeev Joshi,Alex Groce.New Challenges in Model Checking[M].25 Years of Model Checking,2008:65-76.

[12] Mary Jean Harrold.Testing: a roadmap[C]//ICSE - Future of SE Track,2000:61-72.

[13] 蔣凡,談剛.TTCN-3語(yǔ)言編譯器符號(hào)表的設(shè)計(jì)和實(shí)現(xiàn)[J].中國(guó)科學(xué)技術(shù)大學(xué)學(xué)報(bào),2007,37(7):803-806.

[14] 趙會(huì)群,孫晶,張爆,等.嵌入式API測(cè)試套生成方法和技術(shù)[J/OL].軟件學(xué)報(bào),2014,25(2):373-385.http://www.jos.org.cn/1000-9825/4541.htm.

[15] 蘭毓華,毛法堯,曹化工.基于Z規(guī)格說(shuō)明的軟件測(cè)試用例自動(dòng)生成[J].計(jì)算機(jī)學(xué)報(bào),1999,22(9):963-969.

[16] 陳萍,趙會(huì)群,尚思超.一種TTCN測(cè)試套自動(dòng)生成方法研究[J].北京化工大學(xué)學(xué)報(bào),2007,34(S1):64-67.

[17] 趙玉蘭,曾敏,葉新銘.自動(dòng)產(chǎn)生TTCN測(cè)試套以及對(duì)RIP協(xié)議的應(yīng)用[J].內(nèi)蒙古大學(xué)學(xué)報(bào):自然科學(xué)版,2004,25(6):682-687.

RESEARCH ON MODEL CHECKING-GUIDED TTCN-3 TEST SUITE GENERATION TECHNOLOGY

Sun JingJin Xiaowen

(AcademyofInformationEngineering,NorthChinaUniversityofTechnology,Beijing100144,China)

To address the problems of incompleteness and automation of software testing, we proposed to put the model checking in ahead of the customary test in testing process, this combines the model checking with test. Through analysing the formal specification of model checking we cleared the test purpose, and converted it to TTCN-3 (testing and test control notation) abstract test suite. Further, we used the example existing in the specification to associate it with a data type description file, so as to generate test cases. By analysing the TTCN-3 development mode and based on the equivalence of a labelled transition system and TTCN-3 behaviour trees, we put forward a generation algorithm of abstract test suite guided by model checking, and implemented the automatic generation of TTCN-3 abstract test suite.

Software testingModel checkingTTCN-3 test suiteμ-calculus

2014-10-13。

國(guó)家自然科學(xué)基金項(xiàng)目(61070030，6137 0051)；北京市教委人才創(chuàng)新團(tuán)隊(duì)計(jì)劃項(xiàng)目(4062012)。

孫晶，副教授，主研領(lǐng)域：軟件測(cè)試。金曉文，碩士生。

TP3

A

10.3969/j.issn.1000-386x.2016.03.003