《電子技術(shù)應(yīng)用》
您所在的位置:首頁(yè) > 測(cè)試測(cè)量 > 設(shè)計(jì)應(yīng)用 > 一種基于區(qū)域分解的實(shí)時(shí)測(cè)試用例生成技術(shù)研究
一種基于區(qū)域分解的實(shí)時(shí)測(cè)試用例生成技術(shù)研究
宋曉敏,杜軍威
(青島科技大學(xué) 信息科學(xué)與技術(shù)學(xué)院,山東 青島 266061)
摘要: 實(shí)時(shí)系統(tǒng)是指與運(yùn)行環(huán)境的交互行為存在時(shí)間約束的系統(tǒng)。由于時(shí)間約束的無窮狀態(tài)空間問題,增加了實(shí)時(shí)系統(tǒng)測(cè)試難度。本文基于時(shí)間自動(dòng)機(jī),利用時(shí)間區(qū)域分解的方法,將無窮狀態(tài)空間的時(shí)鐘區(qū)域在時(shí)鐘數(shù)量對(duì)應(yīng)的坐標(biāo)圖中等價(jià)劃分為各個(gè)類,在生成的測(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ǔ)。
Abstract:
Key words :

  摘  要實(shí)時(shí)系統(tǒng)是指與運(yùn)行環(huán)境的交互行為存在時(shí)間約束的系統(tǒng)。由于時(shí)間約束的無窮狀態(tài)空間問題,增加了實(shí)時(shí)系統(tǒng)測(cè)試難度。本文基于時(shí)間自動(dòng)機(jī),利用時(shí)間區(qū)域分解的方法,將無窮狀態(tài)空間的時(shí)鐘區(qū)域在時(shí)鐘數(shù)量對(duì)應(yīng)的坐標(biāo)圖中等價(jià)劃分為各個(gè)類,在生成的測(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ǔ)。

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

0 引言

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

  時(shí)間維覆蓋滿足性問題成為基于模型驅(qū)動(dòng)的實(shí)時(shí)測(cè)試的關(guān)鍵問題,常見的基于模型的測(cè)試方法多采用隨機(jī)選取時(shí)間滿足點(diǎn)替代時(shí)間區(qū)間的測(cè)試,或采用狀態(tài)空間與后繼遷移的空間交集分解后再選取隨機(jī)點(diǎn)的方法,這類方法都無法滿足時(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],其中:

 ?。?)L是一個(gè)有限狀態(tài)的集合;

 ?。?)l0是初始狀態(tài),是L的子集;

 ?。?)C是一個(gè)有限的時(shí)鐘集合,所有的時(shí)鐘在l0處初始化為零;

 ?。?)A是一個(gè)有限的標(biāo)記集合;

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

 ?。?)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的語義由一個(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)中有如下兩種類型的遷移[5,7]:

 ?。?)時(shí)間流逝遷移:對(duì)一個(gè)狀態(tài)(s,v)和一個(gè)實(shí)數(shù)的時(shí)間增量d≥0,如果對(duì)所有的d≥d′≥0,v+d′∈l(s),則(s,v)B0%DC18C~ATZ~(E8Q`0SNQ8.jpg(s,v+d);

 ?。?)動(dòng)作遷移:對(duì)于一個(gè)狀態(tài)(s,v)和一個(gè)遷移(s,a,u,λ,s′),其中v∈u,則(s,v)YHDG1O7$3~])`BO6@{6R2U2.png(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ù)部分。為了更好地說明,將區(qū)域劃分為三種類別[1]:拐點(diǎn)區(qū)域、開線段區(qū)域和開區(qū)域。時(shí)鐘區(qū)域的計(jì)算要同時(shí)考慮時(shí)鐘的個(gè)數(shù)以及一個(gè)遷移是輸入還是輸出。CR表示時(shí)鐘區(qū)域的數(shù)目,C表示時(shí)鐘的個(gè)數(shù),Cx、Cy表示時(shí)間約束的長(zhǎng)度。

001.jpg

  當(dāng)時(shí)鐘數(shù)為1,即C=1時(shí),如圖1,給出了此時(shí)的區(qū)域最小數(shù)的情況,區(qū)域數(shù)為4,即2個(gè)拐點(diǎn)區(qū)域+2個(gè)開線段區(qū)域。而當(dāng)Cx增加最小量1時(shí),拐點(diǎn)區(qū)域和開線段區(qū)域都相應(yīng)地增加1,也就是說,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)。

  當(dāng)時(shí)鐘數(shù)為2,即C=2時(shí),時(shí)鐘值用相應(yīng)的二維坐標(biāo)來表示,每個(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)來表示,同樣可以推算出此時(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ù)

 ?。?)首先根據(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來說,系統(tǒng)中的全部可能的狀態(tài)即為q0,q1,q2[8]。然后將全部的狀態(tài)空間按時(shí)間維展開為時(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)的遷移。

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

 ?。?)任取路徑按相應(yīng)時(shí)間維數(shù)的區(qū)域計(jì)算方法,生成路徑上每個(gè)點(diǎn)的時(shí)間區(qū)域類,并按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 案例分析

002.jpg

  對(duì)單一路徑來說,系統(tǒng)中每條路徑中的邊和時(shí)間的取點(diǎn)不盡相同。根據(jù)時(shí)鐘數(shù)量的不同,每個(gè)時(shí)鐘對(duì)應(yīng)的約束不同,其相應(yīng)的取點(diǎn)也就不同,舉一個(gè)簡(jiǎn)單的列車通過道口的例子,如圖3。狀態(tài)A(approach)表示列車接近道口,O(open)表示道口打開,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)列車接近滿足t<5時(shí),道口打開,此時(shí)再判斷t的大小,若是t>3,則列車等待(wait),狀態(tài)由O回到A,重新判斷;若是t<3,狀態(tài)由O遷移到C,則列車通過(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è)試用例:

  (0).open→(0).cross→(1).close

 ?。?).open→(0.5).cross→(1).close

  (0).open→(1).cross→(1).close

 ?。?).open→(1.5).cross→(1).close

 ?。?).open→(2).cross→(1).close

 ?。?).open→(2.5).cross→(1).close

 ?。?).open→(3).cross→(1).close

  (0).open→(3.5).wait

 ?。?).open→(4).wait

4 總結(jié)

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

參考文獻(xiàn)

  [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, Fifth 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. GeTeX: 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.


此內(nèi)容為AET網(wǎng)站原創(chuàng),未經(jīng)授權(quán)禁止轉(zhuǎn)載。