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

　　關(guān)鍵詞： 實時系統(tǒng),；區(qū)域分解,；時間自動機；狀態(tài)空間,；測試用例

0 引言

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

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

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

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

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

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

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

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

　?。?）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ā)生時被重置的時鐘,。

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

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

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

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

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

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

　　當(dāng)時鐘數(shù)為1,，即C=1時，如圖1,，給出了此時的區(qū)域最小數(shù)的情況,，區(qū)域數(shù)為4，即2個拐點區(qū)域+2個開線段區(qū)域,。而當(dāng)Cx增加最小量1時,，拐點區(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）。

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

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

　?。?）首先根據(jù)所給自動機模型的實例，分析系統(tǒng)中全部可能的狀態(tài),。如一個有窮狀態(tài)機[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)的遷移,。

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

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

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

3 案例分析

　　對單一路徑來說，系統(tǒng)中每條路徑中的邊和時間的取點不盡相同,。根據(jù)時鐘數(shù)量的不同,，每個時鐘對應(yīng)的約束不同，其相應(yīng)的取點也就不同,，舉一個簡單的列車通過道口的例子,，如圖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á)起點A，同時,，時間t重新置為0,。

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

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

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

　?。?）.open→（1）.cross→（1）.close

　?。?）.open→（1.5）.cross→（1）.close

　　（0）.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é)

　　本文利用時間自動機模型來描述實時系統(tǒng),，分析系統(tǒng)狀態(tài)空間，提出面向時間維模式的狀態(tài)空間計算方法,，將區(qū)域劃分為不同類別,，簡化了時鐘區(qū)域的取值。然后介紹了計算時鐘區(qū)域數(shù)量的方法,。最后給出具體的生成測試用例的實例,。后期研究內(nèi)容包括對時鐘區(qū)域的進一步劃分，進而減少生成測試用例的數(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,， Fifth Annual IEEE Symposium on e. IEEE,， 1990：414-425.

　　[5] 孫全勇.時間自動機及其應(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] 陳偉,，薛云志,，趙琛，等.一種基于時間自動機的實時系統(tǒng)測試方法[J].軟件學(xué)報,，2007,，18（1）：62-73.

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