模型檢測引導的TTCN-3測試套生成技術研究

孫　晶　金曉文

(北方工業大學信息工程學院　北京 100144)

?

模型檢測引導的TTCN-3測試套生成技術研究

孫晶金曉文

(北方工業大學信息工程學院北京 100144)

針對軟件測試的不完備性以及軟件測試自動化問題，提出在測試過程中將模型檢測前置于傳統測試，將模型檢測與測試相結合。通過分析模型檢測中的形式化規約明確測試目的，并轉換成TTCN-3(Testing and Test Control Notation) 抽象測試套。進一步利用規約中本身存在的正例，與數據類型描述文件相關聯，從而生成測試用例。分析TTCN-3開發模式，基于標簽轉換系統與TTCN-3行為樹的等價性，提出模型檢測引導的抽象測試套生成算法，并實現TTCN-3抽象測試套的自動生成。

軟件測試模型檢測TTCN-3測試套μ演算

0　引　言

近年來，模型檢測以其自動化程度高的特點在軟件測試領域得到了廣泛關注。由于模型檢測可以自動執行，并能在系統不滿足性質時提供反例路徑來說明不滿足的原因，因此在工業界比演繹證明更受推崇。而測試是保證軟件產品可靠性和正確性的傳統手段，相較模型檢測而言自動化不高，手動選取測試用例有不完備性。

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

可是不論是新興的模型檢測還是傳統的軟件測試都有其弊端，模型檢測會由于值域太泛而導致狀態爆炸[11]，而傳統測試又有其不完備性[12]。所以本文提出一種模型檢測引導的TTCN-3測試套生成技術，該技術通過對將軟件的所有狀態轉化成LTS(Label Transition System)，然后根據測試目的對標簽轉換系統進行形式化規約，在明確了測試目的之后進行自動化的軟件測試。

1　TTCN-3概述

TTCN是一個由ETSI(European Telecommunications Standards Institute)維護的全球適用的標準測試語言。在第三代標準中，TTCN-3是一個現代的且靈活的語言，其廣泛的接口機制，被用于描述許多類型的系統測試。典型的應用領域為系統測試、交互性測試、協議測試、業務測試、模塊測試等。

TTCN-3作為標準測試語言，其不僅囊括了普通程序設計語言的簡單明了，易于人機交互。而且其擁有便于測試的功能支持，如動態測試配置、測試判決處理、定時器機制、通信機制等。

TTCN-3連接是端口到端口和端口到測試系統接口的連接。其測試配置如圖1所示。所以從某一方面而言，TTCN-3所描述的測試系統就是根據測試目的進行動態測試配置，并通過定時器機制、通信機制等進行測試并最后進行測試判決處理。

圖1　動態測試配置

用TTCN-3描述測試系統，就是抽象測試套的生成。目前的方式還只是限于手動編寫文本格式的TTCN-3文件，或用GFT圖形化標準進行轉化。但上述兩種方式是人為的，比較被動。由于TTCN-3的層次結構和基本作用域范圍的控制[13]，手動書寫TTCN-3測試套還是存在一定的錯誤和風險。

對于TTCN-3的執行環境，目前在國內外已有研究和應用。如Elvior、OpenTTCN Tester、Testing Technologies公司開發的TTworkbench都是TTCN-3官網上公布的很權威的TTCN-3的編譯、運行環境。而國內， 中國科學技術大學也已開發了協議測試工具——LoongTesting，且兼容了Windows及Linux平臺。

2　TTCN-3測試套的自動生成

2.1模型檢測引導

模型檢測的基本步驟為：建模、規范和驗證。

在建模過程中，需要對系統功能進行描述，常用的一種描述形式是標簽轉換系統LTS。規范是根據測試目的(系統期望滿足的性質)進行形式化描述，之后通過模型檢測工具進行驗證。

例如一個LTS描述的被測系統，狀態S={0,1,2}， 初態I={0}，轉移動作→={<0,1>, <1,1>*,<1,2>}，活動A={a0,a1,a2…,a9}，謂詞P={True,False}。LLTS={, *, }表達了一個活動a0,a1執行的實例，如圖2所示。對于系統的某個功能進行描述，即對標簽轉換系統的某一個性質進行斷言描述，則可描述為：[a0.a1*]true。

圖2　被測系統的LTS描述

本實驗項目組分為三部分，第一部分是對軟件行為和軟件結構的抽象描述，將被測系統用LTS的形式(控制流圖)描述出來，并轉化成為服務描述語言bpel和wsdl進行物理存儲. 第二部分涉及測試目的引導的模型檢測，即通過明確測試目的，轉化為模態邏輯公式μ演算。并與LTS描述的被測系統相結合，進行模型檢測。本文是第三部分，通過分析模型檢測中的形式化規約(μ演算)明確測試目的，自動化轉換成TTCN-3 抽象測試套?？梢钥闯?，經過本項目組其他工作之后，我們已得到了一個構造完整的測試模型。

2.2測試套生成

對TTCN-3測試系統而言，針對特定的被測系統，用戶自定義部分有兩個方面：(1) 根據被測系統測試要求編寫 TTCN-3 測試例；(2) 根據TTCN-3測試例和被測系統編寫或者重用可執行測試套(適配器)[8]。

對于黑盒測試語言TTCN-3而言，首先要明確其測試目的。在項目組第二部分的工作中，已將形式化規約描述的活動序列轉化為μ演算來描述，這就幫助明確了測試目的。因為其只描述了關鍵活動，為了方便理解，可以將其看做是“簡化的LTS”。而基于LTS與TTCN-3行為樹的等價性[14]，提出了抽象測試套生成算法。

算法1抽象測試套生成算法

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}}

//順序結構

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

//分支結構

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

//循環結構

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

//至少執行一次的循環結構

END

END

在提出了算法后，就可以將其進行自動化的轉化，實現可執行測試套的自動生成。我們先從左至右掃描μ演算文件，分離存儲事件(event)和邏輯部分(logic)，并解析相關的bpel文件，根據μ演算與TTCN-3的映射關系，依次生成TTCN-3抽象測試套的主體部分。

do_module();

do_component();

do_function();

do_testcase();

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

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

表1　TTCN-3與μ演算的重要映射關系

μ演算相同的事件門操作(event)會抽象成同一組件的行為，會在同一個函數中來實現。例如，一個μ演算是這樣描述一個系統的["op_1 !Request_1″.″op_1 ?Response_1″]true.系統首先會產生一個主測試成分mtcType,然后根據對應系統描述會產生op_1function(),然后在測試例testcase中根據邏輯生成調用function的關系。

又例如，一個復雜一些的μ演["op_1 !Request_1″.″op_1 ?Response_1″.″op_2 !Request_2″.″op_2 ?Response_2″]true，則會對應倆個函數function,分別為op_1function() 和op_2function()，測試套中表現了函數之間的調用關系?？梢钥闯鰧τ谏鲜靓萄菟銟永?，邏輯關系是順序的，且對應描述如下：

testcase TC_0() runs on mtcType{

op_1function();

op_2function();

}

3　測試例的自動生成

在構造完測試模型之后，我們的任務就是生成和執行測試例[10]。由于傳統測試中的不完備性，對于測試例的選取有局限性。模型檢測自動化全部遍歷所有空間狀態，可以對所有的活動序列的屬性進行形式化規約，并檢測出不符合形式化規約的反例路徑，這就借鑒了傳統的基于模型檢測的測試用例自動生成的方法，而與此同時應該注意到形式化規約中，是存在正例路徑的，所以拓展這一部分，并將得到的模型檢測的結果與相關的數據類型描述文件(bpel組合中的wsdl)進行關聯，解析bpel中名稱空間里wsdl的位置(lns)，同時根據需要獲取數據類型的消息名稱來提取測試用例。

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

[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)驗證了水是TSR反應發生的必要條件，在無水條件下 ，CaSO4不能引發TSR反應生成H 2 S。

PortType_1

Operation Name:

op_1

Messages:

Request_1

parameter name:i parameter type:integer

可以看出根據wsdl提取出了變量的數據類型，最后依照傳統測試中等價類劃分的方法提取測試用例，嵌入到之前已經生成好的抽象測試套的邏輯框架中。對于復雜數據類型如record等，提供了數據模板模塊，用戶可以根據測試需求與模板格式進行手動加載。

4　案例研究與評估

4.1案例研究

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

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

如果針對主程序進行完整測試，則對應μ演算描述為：

[″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

通過分析上述形式化規約，和前期已經生成好的被測系統的形式化描述文件bpel和wsdl，自動生成測試套。由于測試套龐大復雜，在此只列出測試套的數據類型定義如圖4及測試例如圖5所示。

圖4　數據類型定義　　　　　　　圖5　測試例

將生成的測試套加載在TTCN-3編譯運行環境中進行驗證，并根據被測系統編寫配套的編解碼器和適配器。得到運行結果如圖6所示，可以看到定時器啟用了164次符合邏輯預期。

4.2評估

在經過大量的學習和助教工作之后，我們發現手動編寫TTCN-3測試套是需要大量的前期投入的，這包括對于人員的技術培訓、實驗環境的搭建等等。

圖7　手動/自動效率對比圖

在明確測試目的的前提下，對手動編寫TTCN-3測試套(在保證準確的情況下)和本文中提到的自動生成TTCN-3測試套(包括配置路徑的時間)進行了效率對比，如圖7針對同一源代碼，生成同一測試套，然后對比其所用時間?？梢钥闯鍪謩泳帉憸y試套的方法所用的時間會隨著被測系統規模的增長呈幾近指數型增長，而自動生成的時間增長并不明顯。

5　結　語

關于TTCN-3測試套自動生成以及測試例生成的研究有許多。蘭毓華等人[15]提出了一種基于 Z 規格說明的軟件測試用例自動生成方法， 通過對軟件Z規格說明的分析，找出描述軟件輸入、 輸出約束的線性謂詞，經過線性謂詞轉換， 線性謂詞到線性不等式組的轉換， 找出區域邊界頂點和邊界附近的測試點等過程自動生成測試用例。陳萍等[16]提出了根據 TTCN-3標準的第三部分GFT與TTCN-3核心語言的內在關聯以及標準中的語法規定的一種TTCN-3測試套生成方法，并設計開發了一套由圖形表示格式自動生成用核心語言描述的測試套的轉換工具。趙玉蘭等[17]介紹一個在GE-LOTOS的基礎上自動產生TTCN測試套的工具， 該工具是基于由形式描述技術語言E-LOTOS轉換成的GE-LOTOS。 并對 Internet上的一個標準路由信息協議(RIP協議)進行了TTCN測試套的應用。

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

本文的不足之處在于只能生成簡單數據類型的測試用例。但也基本上規避了顏烔[10]等在基于模型的軟件測試綜述一文中提到的基于模型的軟件測試的缺點，即狀態空間爆炸問題。而傳統的手動編寫TTCN-3測試套的模式效率不高，本文中提出的自動化生成的模式一定程度上提高了測試套生成的效率。

[1] 林惠民,張文輝.模型檢測:理論、方法與應用[J].電子學報,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] 蘇開樂,駱翔宇,呂關鋒.符號化模型檢測CTL[J].計算機學報,2005,28(11):1798-1806.

[6] 何愷鐸,顧明,宋曉宇,等.面向源代碼的軟件模型檢測及其實現[J].計算機科學,2009,36(1):267-272.

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

[8] 劉小勇,蔣凡.TTCN-3測試套開發模式及其應用[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] 顏炯,王戟,陳火旺.基于模型的軟件測試綜述[J].計算機科學,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語言編譯器符號表的設計和實現[J].中國科學技術大學學報,2007,37(7):803-806.

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

[15] 蘭毓華,毛法堯,曹化工.基于Z規格說明的軟件測試用例自動生成[J].計算機學報,1999,22(9):963-969.

[16] 陳萍,趙會群,尚思超.一種TTCN測試套自動生成方法研究[J].北京化工大學學報,2007,34(S1):64-67.

[17] 趙玉蘭,曾敏,葉新銘.自動產生TTCN測試套以及對RIP協議的應用[J].內蒙古大學學報:自然科學版,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。

國家自然科學基金項目(61070030，6137 0051)；北京市教委人才創新團隊計劃項目(4062012)。

孫晶，副教授，主研領域：軟件測試。金曉文，碩士生。

TP3

A

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