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

宋曉敏，杜軍威

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

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

宋曉敏，杜軍威

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

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

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

0 引言

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

3 案例分析

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

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

圖3 列車(chē)通過(guò)道口實(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é)

本文利用時(shí)間自動(dòng)機(jī)模型來(lái)描述實(shí)時(shí)系統(tǒng)，分析系統(tǒng)狀態(tài)空間，提出面向時(shí)間維模式的狀態(tài)空間計(jì)算方法，將區(qū)域劃分為不同類(lèi)別，簡(jiǎn)化了時(shí)鐘區(qū)域的取值。然后介紹了計(jì)算時(shí)鐘區(qū)域數(shù)量的方法。最后給出具體的生成測(cè)試用例的實(shí)例。后期研究?jī)?nèi)容包括對(duì)時(shí)鐘區(qū)域的進(jìn)一步劃分，進(jìn)而減少生成測(cè)試用例的數(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]孫全勇.時(shí)間自動(dòng)機(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]陳偉，薛云志，趙琛，等.一種基于時(shí)間自動(dòng)機(jī)的實(shí)時(shí)系統(tǒng)測(cè)試方法[J].軟件學(xué)報(bào)，2007，18（1）：62-73.

[8]MATHUR A P.軟件測(cè)試基礎(chǔ)教程[M].王峰，郭長(zhǎng)國(guó)，陳振華，等，譯.北京：機(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-），女，在讀碩士生，主要研究方向：軟件測(cè)試。

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

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