一種基于區(qū)域分解的實(shí)時測試用例生成技術(shù)研究*

宋曉敏，杜軍威

（青島科技大學(xué)信息科學(xué)與技術(shù)學(xué)院，山東青島266061）

一種基于區(qū)域分解的實(shí)時測試用例生成技術(shù)研究*

宋曉敏，杜軍威

（青島科技大學(xué)信息科學(xué)與技術(shù)學(xué)院，山東青島266061）

實(shí)時系統(tǒng)是指與運(yùn)行環(huán)境的交互行為存在時間約束的系統(tǒng)。由于時間約束的無窮狀態(tài)空間問題，增加了實(shí)時系統(tǒng)測試難度。本文基于時間自動機(jī)，利用時間區(qū)域分解的方法，將無窮狀態(tài)空間的時鐘區(qū)域在時鐘數(shù)量對應(yīng)的坐標(biāo)圖中等價劃分為各個類，在生成的測試路徑中取到相應(yīng)的點(diǎn)坐標(biāo)，簡化取點(diǎn)的個數(shù)，有效減少測試用例的生成數(shù)量，進(jìn)而相對減少狀態(tài)空間爆炸的可能性，為實(shí)時系統(tǒng)功能、安全性驗(yàn)證提供理論基礎(chǔ)。

實(shí)時系統(tǒng)；區(qū)域分解；時間自動機(jī)；狀態(tài)空間；測試用例

0 引言

隨著計(jì)算機(jī)系統(tǒng)在航空航天、軌道交通、工業(yè)控制和核反應(yīng)控制等安全苛求系統(tǒng)中的廣泛應(yīng)用，如何有效地保障這類系統(tǒng)的安全性與可靠性成為行業(yè)著重解決的關(guān)鍵問題。而實(shí)時性是影響這類系統(tǒng)安全性的關(guān)鍵特性，如何檢測和驗(yàn)證該類系統(tǒng)滿足實(shí)時性能需求成為保證系統(tǒng)安全的關(guān)鍵技術(shù)。而實(shí)時系統(tǒng)因增加時間約束，加速了這類系統(tǒng)狀態(tài)空間爆炸，而無法保證這類系統(tǒng)的完備測試和驗(yàn)證。常見的該類系統(tǒng)的測試方法主要包括靜態(tài)時間分析和動態(tài)實(shí)時測試。靜態(tài)分析方法通過預(yù)估計(jì)程序執(zhí)行的時間判定時間約束的滿足性；動態(tài)測試是在系統(tǒng)仿真執(zhí)行時調(diào)用時鐘部件進(jìn)行任務(wù)執(zhí)行時間測算，從而判定時間約束的滿足性。但這類測試方法難以應(yīng)用到基于模型驅(qū)動的實(shí)時測試問題中。

時間維覆蓋滿足性問題成為基于模型驅(qū)動的實(shí)時測試的關(guān)鍵問題，常見的基于模型的測試方法多采用隨機(jī)選取時間滿足點(diǎn)替代時間區(qū)間的測試，或采用狀態(tài)空間與后繼遷移的空間交集分解后再選取隨機(jī)點(diǎn)的方法，這類方法都無法滿足時間點(diǎn)覆蓋需求。本文提出一種基于時間自動機(jī)模型的測試用例生成方法，將時鐘區(qū)域等價劃分，使得每個區(qū)域的時鐘值表示相同行為[1]，生成數(shù)量少、覆蓋點(diǎn)完備的測試用例集合。

1 時間自動機(jī)[2-4]及其狀態(tài)空間

對于時鐘集合C，時鐘約束[3，5]集合Ф（C）={Ф|Ф是一個時鐘約束}，其中Ф是時間自動機(jī)的基本組成成分，是實(shí)時系統(tǒng)模型檢查算法操作的基礎(chǔ)，定義：Ф=x∞n|x-y∞n∞，x、y∈C，n∈N。

一個時間自動機(jī)T可以表示為一個多元組（L，l0，C，A，E，I）[1，2，6]，其中：

（1）L是一個有限狀態(tài)的集合；

（2）l0是初始狀態(tài)，是L的子集；

（3）C是一個有限的時鐘集合，所有的時鐘在l0處初始化為零；

（4）A是一個有限的標(biāo)記集合；

（5）E是一個映射，給每一個位置L指定Ф（C）中的某個時鐘約束；

（6）I是一個狀態(tài)遷移的集合，其中E?L×A×2C×Ф（C）×L。一個遷移（s，a，u，λ，s′）表示當(dāng)輸入符號a時從狀態(tài)s轉(zhuǎn)移到狀態(tài)s′，u是X上的一個時鐘約束條件，即u∈Ф（C），它指定遷移的發(fā)生時間，集合λ∈X給出在狀態(tài)轉(zhuǎn)移發(fā)生時被重置的時鐘。

時間自動機(jī)T的語義由一個與它相關(guān)的系統(tǒng)S定義，其狀態(tài)擴(kuò)展為＜s，v＞，其中s為A的某一狀態(tài)，v是一個時鐘解釋。如果s是A的初始位置，并且對于所有的時鐘變量x都有v（x）=0，那么狀態(tài)（v，s）便是一個初始狀態(tài)。在遷移系統(tǒng)中有如下兩種類型的遷移[5，7]：

（1）時間流逝遷移：對一個狀態(tài)（s，v）和一個實(shí)數(shù)的時間增量d≥0，如果對所有的d≥d′≥0，v+d′∈l（s），則（s，v）→d（s，v+d）；

（2）動作遷移：對于一個狀態(tài)（s，v）和一個遷移（s，a，u，λ，s′），其中v∈u，則（s，v）→a（s′，v′）。

2 時間狀態(tài)空間的計(jì)算及測試用例生成技術(shù)

2.1 時間狀態(tài)空間的計(jì)算

劃分時鐘區(qū)域要求時間的整數(shù)部分一致，并且所有時鐘間的小數(shù)部分的變化順序也一致。整數(shù)部分決定是否滿足指定的時鐘約束，而小數(shù)部分的先后順序決定哪個時鐘會先改變其整數(shù)部分。為了更好地說明，將區(qū)域劃分為三種類別[1]：拐點(diǎn)區(qū)域、開線段區(qū)域和開區(qū)域。時鐘區(qū)域的計(jì)算要同時考慮時鐘的個數(shù)以及一個遷移是輸入還是輸出。CR表示時鐘區(qū)域的數(shù)目，C表示時鐘的個數(shù)，Cx、Cy表示時間約束的長度。

當(dāng)時鐘數(shù)為1，即C=1時，如圖1，給出了此時的區(qū)域最小數(shù)的情況，區(qū)域數(shù)為4，即2個拐點(diǎn)區(qū)域+2個開線段區(qū)域。而當(dāng)Cx增加最小量1時，拐點(diǎn)區(qū)域和開線段區(qū)域都相應(yīng)地增加1，也就是說，Cx每增加1，區(qū)域總數(shù)CR相應(yīng)增加2。由此可以得到，當(dāng)只有一個時鐘即C=1時，區(qū)域總數(shù)CR=4+（2×（Cx-1））=2×（Cy+1）。

圖1 時鐘數(shù)為1時的區(qū)域劃分圖

圖2 時鐘數(shù)為2時的區(qū)域劃分圖

當(dāng)時鐘數(shù)為2，即C=2時，時鐘值用相應(yīng)的二維坐標(biāo)來表示，每個坐標(biāo)軸代表一個時鐘，如圖2給出了當(dāng)Cx=Cy=1時的最小區(qū)域數(shù)。從圖中可以看出此時的區(qū)域個數(shù)為18，可以推算出當(dāng)時鐘數(shù)C=2時，區(qū)域總數(shù)CR=（6×Cx×Cy）+4×（Cx+Cy+1）。

當(dāng)時鐘數(shù)為3，即C=3時，時鐘值用相應(yīng)的三維坐標(biāo)來表示，同樣可以推算出此時的區(qū)域總數(shù)CR=（22× Cx×Cy×Cz）+10×（Cx×Cy+Cx×Cz+Cy×Cz）+8×（Cx+Cy+ Cz+1）[1]。

劃分的區(qū)域可以簡化取點(diǎn)的個數(shù)，進(jìn)而減少生成的測試用例的數(shù)量。例如若在圖2中取點(diǎn)（0.65，0.5）和（0.72，0.6），根據(jù)上述的等價劃分方法，在這里可認(rèn)為二者是等價的，即二者對應(yīng)生成的路徑是一樣的。

2.2 測試用例生成技術(shù)

（1）首先根據(jù)所給自動機(jī)模型的實(shí)例，分析系統(tǒng)中全部可能的狀態(tài)。如一個有窮狀態(tài)機(jī)[8]M（X，Y，Q，q0，ε，O），其中X={a，b}是一個輸入符號集合，Y={0，1}是一個輸出符號集合，Q={q0，q1，q2}是一個有窮的狀態(tài)集合，q0是初始狀態(tài)，ε是狀態(tài)轉(zhuǎn)換函數(shù)，O是輸出函數(shù)。對M來說，系統(tǒng)中的全部可能的狀態(tài)即為q0，q1，q2[8]。然后將全部的狀態(tài)空間按時間維展開為時間狀態(tài)空間。即將模型中的各個狀態(tài)位置分別和一個時間域一起構(gòu)成符號狀態(tài)以生成有限狀態(tài)模型，也就是對位置賦一個時間不變量。遷移動作發(fā)生時的時鐘值需要滿足一定的約束條件，才能發(fā)生狀態(tài)的遷移。

（2）由時間狀態(tài)空間生成相應(yīng)的路徑。當(dāng)滿足發(fā)生遷移的時間約束和遷移約束時，遷移發(fā)生，從一個狀態(tài)遷移到另一個狀態(tài)，最終形成路徑。

（3）任取路徑按相應(yīng)時間維數(shù)的區(qū)域計(jì)算方法，生成路徑上每個點(diǎn)的時間區(qū)域類，并按2.1節(jié)中介紹到的區(qū)域點(diǎn)選取規(guī)則，產(chǎn)生該點(diǎn)的區(qū)域樣點(diǎn)。

（4）根據(jù)每條路徑的約束規(guī)則，選取路徑點(diǎn)的時間樣點(diǎn)的組合點(diǎn)，形成該條路徑的滿足時間維的測試用例。

3 案例分析

對單一路徑來說，系統(tǒng)中每條路徑中的邊和時間的取點(diǎn)不盡相同。根據(jù)時鐘數(shù)量的不同，每個時鐘對應(yīng)的約束不同，其相應(yīng)的取點(diǎn)也就不同，舉一個簡單的列車通過道口的例子，如圖3。狀態(tài)A（approach）表示列車接近道口，O（open）表示道口打開，C（close）表示道口關(guān)閉，即狀態(tài)Q={A，O，C}有三個。當(dāng)滿足時間約束t＜3時，狀態(tài)由A遷移到O，此時時間重置為0。當(dāng)列車接近滿足t＜5時，道口打開，此時再判斷t的大小，若是t＞3，則列車等待（wait），狀態(tài)由O回到A，重新判斷；若是t＜3，狀態(tài)由O遷移到C，則列車通過（cross），此時t重置為0。若t＜2則道口關(guān)閉（close），狀態(tài)C到達(dá)起點(diǎn)A，同時，時間t重新置為0。

對應(yīng)上例，根據(jù)2.1節(jié)介紹的區(qū)域點(diǎn)選取規(guī)則，可能會生成如下的測試用例：

圖3 列車通過道口實(shí)例

（0）.open→（0）.cross→（1）.close

（0）.open→（0.5）.cross→（1）.close

（0）.open→（1）.cross→（1）.close

（0）.open→（1.5）.cross→（1）.close

（0）.open→（2）.cross→（1）.close

（0）.open→（2.5）.cross→（1）.close

（0）.open→（3）.cross→（1）.close

（0）.open→（3.5）.wait

（0）.open→（4）.wait

4 總結(jié)

本文利用時間自動機(jī)模型來描述實(shí)時系統(tǒng)，分析系統(tǒng)狀態(tài)空間，提出面向時間維模式的狀態(tài)空間計(jì)算方法，將區(qū)域劃分為不同類別，簡化了時鐘區(qū)域的取值。然后介紹了計(jì)算時鐘區(qū)域數(shù)量的方法。最后給出具體的生成測試用例的實(shí)例。后期研究內(nèi)容包括對時鐘區(qū)域的進(jìn)一步劃分，進(jìn)而減少生成測試用例的數(shù)量。

[1]ABOUTRAB M S.Testing real-time embedded systems using timed automata based approaches[J].The Journal of Systems and Software 2013（86）：1209-1216.

[2]ALUR R，DILL D L.A theory of timed automata[J].Theoretical Computer Science，1994，126（2）：183-235.

[3]ALUR R.Timed automata[J].Computer Aided Verification. Springer Berlin Heidelberg，1999：8-22.

[4]ALUR R，COURCOUBETIS C，DILL D.Model-checking for real-time systems[C].Logic in Computer Science，1990，LICS′90，Proceedings，F(xiàn)ifth Annual IEEE Symposium on e.IEEE，1990：414-425.

[5]孫全勇.時間自動機(jī)及其應(yīng)用研究[D].哈爾濱：哈爾濱工程大學(xué)，2007.

[6]ABOUTRAB M S，COUNSELL S，HIEROINS R M.Ge-TeX：a tool for testing real-time embedded systems using CAN applications[C].18th IEEE International Conference and Workshops on Engineering of Computer-Based Systems，2011：61-70.

[7]陳偉，薛云志，趙琛，等.一種基于時間自動機(jī)的實(shí)時系統(tǒng)測試方法[J].軟件學(xué)報(bào)，2007，18（1）：62-73.

[8]MATHUR A P.軟件測試基礎(chǔ)教程[M].王峰，郭長國，陳振華，等，譯.北京：機(jī)械工業(yè)出版社，2011.

A real-time test case generation technology based on domain decom position

Song Xiaomin，Du Junwei
（School of Information Science&Technology，Qingdao University of Science&Technology，Qingdao 266061，China）

Real-time systems are the systems which have time constraints when interacting with the runtime environment.The infinite state space of time constraints increases the difficulty of testing the real-time system.Based on a timed automata，using the method of time domain decomposition，the infinite state space of the clock area is divided into various classes equivalently in the clock number corresponding coordinate diagram.Taking the corresponding point coordinates in the generated test path，simplifying the number of point，so the number of generated test cases is reduced effectively，and then the possibility of state space explosion is reduced relatively.It can also provide theoretical basis for the function and safety verification of real-time system.

real-time systems；domain decomposition；timed automata；state space；test case

TP306+.2

A

1674-7720（2015）09-0029-03

2015-01-07）

宋曉敏（1988-），女，在讀碩士生，主要研究方向：軟件測試。

國家自然科學(xué)基金資助項(xiàng)目（61273180）；山東省自然基金項(xiàng)目（ZR2012FL17）

杜軍威（1974-），男，博士，教授，主要研究方向：軟件的可信性分析與驗(yàn)證。