高　莉

(安徽建筑大學 電子與信息工程學院計算機系，安徽 合肥　230601)

?

基于LTL的UML狀態(tài)圖測試用例生成方法

高莉

(安徽建筑大學 電子與信息工程學院計算機系，安徽 合肥230601)

摘要：測試用例的自動生成是軟件測試研究的主要方向之一，針對軟件開發(fā)過程中測試數(shù)據(jù)生成存在低效、無目的、冗余等問題，提出了基于UML狀態(tài)模型圖的面向?qū)ο箢惣墱y試用例生成方法，將UML狀態(tài)圖轉(zhuǎn)換成相應的事件確定有限狀態(tài)機，通過線性時序邏輯的模型檢測技術(shù)，驗證有限狀態(tài)機模型的正確性，實驗結(jié)果表明，該方法能夠在不降低遷移覆蓋準則的情況下，生成數(shù)量少、針對性強的測試用例集。

關(guān)鍵詞：軟件測試；測試用例生成；UML狀態(tài)圖；線性時序邏輯

0引言

軟件測試，是軟件生命周期的重要組成部分，如何生成滿足一定測試覆蓋準則、數(shù)量少、針對性強的測試用例，一直以來都是軟件測試的研究熱點。統(tǒng)一建模語言UML是在Booch、OMT、OOSE等面向?qū)ο蟮姆椒捌渌S多方法與資料的基礎(chǔ)上發(fā)展起來的，UML的九類模型圖貫穿于整個軟件設(shè)計周期，而基于UML模型圖自動構(gòu)造測試用例，也已經(jīng)成為軟件測試用例生成研究方向的一個重要分支。

目前，國內(nèi)外在基于UML狀態(tài)圖根據(jù)對象的狀態(tài)行為驅(qū)動測試用例生成方面做了大量的研究工作，Supaporn等提出了一種state chart到TFG測試流圖，從而產(chǎn)生測試序列的方法，但沒有考慮測試數(shù)據(jù)的產(chǎn)生；Jeff Offutt和Abdurazik開發(fā)了基于Rational Rose的測試用例生成的驗證工具，但沒有處理轉(zhuǎn)換的監(jiān)護條件; Mcminn等提出了一種基于UML的啟發(fā)式搜索算法，但算法是根據(jù)狀態(tài)變量生成測試用例，對狀態(tài)之間的行為捕捉不足；Cali等提出了基于UML類圖的形式化方法，更傾向于方法理論的研究，研究成果的應用方案沒有具體涉及。

UML狀態(tài)圖(Statechart)描述了面向?qū)ο箢惖囊粋€對象在其生存期間的行為，一個特定對象的所有可能的狀態(tài)以及引起狀態(tài)轉(zhuǎn)移的事件，通過對對象的生存周期建立模型，從而來描述對象隨時間變化的動態(tài)行為。[5-6]本文將UML和形式化技術(shù)相結(jié)合，將狀態(tài)圖轉(zhuǎn)化為有限狀態(tài)機，建立狀態(tài)圖與精確語義定義之間的映射關(guān)系，再通過線性時序邏輯的模型檢測技術(shù)，為測試用例的生成、分析與驗證奠定基礎(chǔ)。

1基于UML的狀態(tài)圖測試用例生成

EFSM是傳統(tǒng)的有限狀態(tài)機(Finite State Machine，F(xiàn)SM)的擴展，文中將EFSM作為描述UML狀態(tài)圖的形式化模型，EFSM中一個狀態(tài)變遷描述了一次信息交互，對象在其生命周期中，通過消息序列的傳遞，產(chǎn)生狀態(tài)的變遷，從而刻畫系統(tǒng)行為的交互過程，將狀態(tài)圖轉(zhuǎn)化成精確的形式化定義，消除了并發(fā)層次狀態(tài)結(jié)構(gòu)，根據(jù)EFSM的路徑，生成滿足遷移測試標準基于數(shù)據(jù)流的測試用例數(shù)據(jù)集合。

定義1狀態(tài)確定有限確定狀態(tài)機D是一個六元組，即D=(C，S,，R，E，Ts，n)

C=S∪R， S∩R=?

式中：C是狀態(tài)圖中可以到達的最大狀態(tài)集合，S是有窮初始狀態(tài)集合，R是有窮遷移狀態(tài)集合，E是觸發(fā)狀態(tài)變遷的事件，Ts是從S到R的函數(shù)關(guān)系，n是狀態(tài)變遷的標號，將第一個發(fā)生的狀態(tài)變遷標記為1，第二個發(fā)生的狀態(tài)變遷標記為2，并依此進行遞推。圖1給出了一個過程加載時的Compiler對象信息的狀態(tài)圖。

圖1過程加載狀態(tài)圖

表1是根據(jù)EFSM模型的規(guī)格說明信息構(gòu)造的二維表，表的行表示目標狀態(tài)集合，列表示源狀態(tài)集合，行與列的交叉點表示從源狀態(tài)集合到目標狀態(tài)集合對應的所有變遷的集合。

表1　擴展的有限狀態(tài)機變遷與狀態(tài)集合的關(guān)系

2基于LTL的狀態(tài)圖驗證

線性時序邏輯(Linear-time Temporary Logic，LTL)，比古典命題邏輯增加了相應的時序算子，時序修飾符用于描述計算樹(Computation tree)上某條路徑的特定性質(zhì)，包括：○(next)，◇(existential)，□(global)，U(until)，R(release)。[7-8]LTL 能夠?qū)ο到y(tǒng)的不同抽象層次進行邏輯描述，通過邏輯蘊涵來進行從需求分析到實現(xiàn)模型的性質(zhì)驗證與一致性驗證，通過驗證狀態(tài)圖的屬性是否滿足LTL性質(zhì)描述語言的特征，在統(tǒng)一的語義框架中逐步細化的進行模型正確性檢查，從而保證軟件設(shè)計滿足系統(tǒng)設(shè)計的需求。

2.1　語法描述

LTL的語法描述為：

X∷=x|﹁X1|X1∨X2|X1∧X2|X1→X2| (X1,…, Xm) prj Y，其中x∈原子命題，,prj 是時序算子，﹁、∧和∨與經(jīng)典邏輯中的定義相同，X1,…, Xm 和Y均為LTL公式。每一個LTL公式都可以通過有限次的應用規(guī)則來構(gòu)造獲得。

2.2　驗證步驟

LTL適用于模型的驗證與檢測，廣泛應用于有限狀態(tài)機的行為描述?；诰€性時序邏輯實現(xiàn)狀態(tài)圖驗證的方法為：通過形式化定義描述系統(tǒng)的規(guī)范，構(gòu)建一種算法滿足一定的測試覆蓋率，遍歷實現(xiàn)模型，從而驗證有限狀態(tài)系統(tǒng)的模型符合系統(tǒng)的規(guī)范說明，可以滿足狀態(tài)圖所表達的性質(zhì)，如果無法驗證該公式的正確性，系統(tǒng)會通過給出一個該屬性的反例，說明模型和性質(zhì)不一致，從而讓用戶找到原因。具體驗證步驟如圖2所示。

圖2驗證步驟

3測試用例生成

UML狀態(tài)圖是展示狀態(tài)與狀態(tài)轉(zhuǎn)換的圖，將其形式化定義之后，在擴展的有限狀態(tài)機上基于控制流進行轉(zhuǎn)換路徑的測試分析，可以從每個轉(zhuǎn)換路徑獲取對應的測試用例，用來檢測被測系統(tǒng)是否存在有這樣的目標程序路徑。轉(zhuǎn)換路徑CP是(Ci,Ti)的集合，其中，Ci∈C，Ti∈Ts，1≤i≤n。算法1是一個搜索算法，從初始狀態(tài)出發(fā)，通過遍歷有限狀態(tài)機包含的所有狀態(tài)點，獲取全部的目標程序路徑，構(gòu)造出滿足軟件測試遷移覆蓋標準的測試用例集合。

算法1

PROCBFS_TREE(TT：EFSM)

BEGIN

VISITE(s0)；

INIQUEUE(Q)；/*初始化設(shè)置空隊列Q*/

ENQUEUE(Q,s0)；/*s0進隊列Q*/

WHILENOT EMPTY(Q)DO

BEGIN

v:=DLQUEUE(Q)；/*隊列頭元素v出隊列*/

FOR每個 ti∈TsDO

IFt沒有被訪問過 且 t.si=vDO

BEGIN

VISITE(t. si′)

ENQUEUE(Q,t. si′)

END

END

ENDP

由擴展的有限狀態(tài)機根據(jù)算法1構(gòu)造出的測試樹如下圖3所示。

圖3測試樹

通過對擴展的有限狀態(tài)機的遍歷，產(chǎn)生了相應的測試樹，得到了對應于狀態(tài)圖的所有路徑，圖3測試樹上所有路徑構(gòu)成的集合為{TP1，TP2}，其中

TP1=(C0，t1)，(C1，t3)，(C2，t2)

TP2=(C0，t1)，(C1，t4)，(C3，t5)

滿足測試覆蓋標準中的遷移覆蓋標準，則由擴展的有限狀態(tài)機就可以產(chǎn)生滿足遷移覆蓋標準的測試用例。待驗證系統(tǒng)中所有的初始狀態(tài)，接受外部觸發(fā)事件，激活系統(tǒng)發(fā)生狀態(tài)的轉(zhuǎn)換，將用例集合加以測試，查看系統(tǒng)狀態(tài)與測試案例的目標狀態(tài)是否匹配，進而確認待驗證系統(tǒng)設(shè)計與實現(xiàn)的一致性。表2列出了算法1對應的測試用例，表3則是列出了根據(jù)深度優(yōu)先搜索獲得的滿足狀態(tài)覆蓋標準的測試用例，可以看出由算法1獲得的測試線索更加全面，涵蓋了對應狀態(tài)圖的所有測試路徑，包含的模型信息更加豐富，覆蓋了對應的狀態(tài)轉(zhuǎn)換觸發(fā)條件，可以更加有效的保證測試的充分性。

表2　滿足遷移覆蓋標準的測試用例

表3　滿足狀態(tài)覆蓋標準的測試用例

4結(jié)束語

軟件測試的核心技術(shù)是能夠自動生成有效的、滿足測試覆蓋準則的測試用例集合，從而提高軟件測試的效率與質(zhì)量，測試過程完全自動化，無需人為干預。本文從UML2.0狀態(tài)模型圖出發(fā)，通過形式化定義，將其轉(zhuǎn)換為有限狀態(tài)機，通過線性時序邏輯驗證有限狀態(tài)機與系統(tǒng)需求的一致性，保證了測試用例生成所需模型的正確，遍歷實現(xiàn)模型，進而生成測試用例集合。進一步的工作是在保證測試用例有效性的前提下，對算法進行優(yōu)化。

參考文獻

1Supaporn K, Wanchai R. Automated-Generating Test Case using UML Statechart Diagrams Proceedings of SAICSIT 2003,296-300.

2Jefferson Offutt A, Liu Shaoying , Aynur Abdurazik,etal. Generating test data from state-based specifications . Soft-ware Testing Verification & Reliability,2003, 13(1):25-53.

3McMinn P. Search-based Software Test Data Generation: A Survey.Software Testing, Verification and Reliability.2004,14(2):105-156

4Cali A, Calvanese D, De Giancomo G ,etal. A formal framework for reasoning on UML class diagrams//proceedings of the Thirteenth International Symposium on Methodologies for Intelligent Systems(ISMIS 2002),volume 2366 of Lecture Notes in Computer Science, Springer, 2002:503-513

5章濤，顧慶，陳道蓄.基于UML狀態(tài)圖的測試技術(shù)研究.計算機科學，2007，34(10)：264-267

6曾一, 王翠欽, 李函逾, 等. 基于UML交互概覽圖的測試線索的生成方法.計算機應用,2014,34(1):270-275,291

7DUAN Zhenhua, TIAN Cong, ZHANG Li. A decision procedure for propositional projection temporal logic with infinite models . Acta Informatica, 2008, 45(1): 43-78.

8Alhroob, A Dahal, K Hossain A. Transforming UML sequence diagram to high level petri net. Proc of 2010 2nd International Conference on Software Technology and Engineering.Puerto Rico USA:ICSTE, 2010.260-264

Test Cases Generation Method from UML Statechart Based on LTL

GAO Li

(Department of Computer Science Electronic and Information Engineering

Institute，Anhui Jianzhu University , Hefei ,Anhui 230601,China)

Abstract:Automatic generation of test cases is one of the main directions of research in software testing. For software development process inefficiencies exist in test data generation, no purpose, redundancy and other issues, proposed test case generation method based on object-oriented class-level UML state chart. UML state chart is converted into the corresponding event deterministic finite state machine, by Linear-time Temporary Logic model checking techniques to verify the correctness of the finite state machine model. The experimental results show that this method can meet the migration standard coverage metric, to generate the number of small, targeted test set.

Key words:software testing; test case generation; UML state chart; LTL

中圖分類號：TP31

文獻標識碼：A

文章編號：2095-8382(2015)02-075-04

DOI：10.11921/j.issn.2095-8382.20150216

作者簡介：高莉(1979-),女, 碩士, 講師，研究領(lǐng)域為智能軟件、軟件的測試與驗證技術(shù)。

基金項目：國家科技支撐計劃(2012BAJ08B00); 安徽高校省級自然科學研究重點項目(KJ2009A018Z)；校青年科研專項經(jīng)費(201183-14).

收稿日期：2014-10-05