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

　　關鍵詞： 實時系統；區域分解；時間自動機；狀態空間；測試用例

0 引言

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

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

1 時間自動機[2-4]及其狀態空間

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

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

　　（1）L是一個有限狀態的集合；

　　（2）l0是初始狀態，是L的子集；

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

　　（4）A是一個有限的標記集合；

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

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

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

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

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

2 時間狀態空間的計算及測試用例生成技術

　　2.1 時間狀態空間的計算

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

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

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

　　當時鐘數為3，即C=3時，時鐘值用相應的三維坐標來表示，同樣可以推算出此時的區域總數CR=（22×Cx×Cy×Cz）+10×（Cx×Cy+Cx×Cz+Cy×Cz）+8×（Cx+Cy+Cz+1）[1]。

　　劃分的區域可以簡化取點的個數，進而減少生成的測試用例的數量。例如若在圖2中取點（0.65，0.5）和（0.72，0.6），根據上述的等價劃分方法，在這里可認為二者是等價的，即二者對應生成的路徑是一樣的。

　　2.2 測試用例生成技術

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

　　（2）由時間狀態空間生成相應的路徑。當滿足發生遷移的時間約束和遷移約束時，遷移發生，從一個狀態遷移到另一個狀態，最終形成路徑。

　　（3）任取路徑按相應時間維數的區域計算方法，生成路徑上每個點的時間區域類，并按2.1節中介紹到的區域點選取規則，產生該點的區域樣點。

　　（4）根據每條路徑的約束規則，選取路徑點的時間樣點的組合點，形成該條路徑的滿足時間維的測試用例。

3 案例分析

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

　　對應上例，根據2.1節介紹的區域點選取規則，可能會生成如下的測試用例：

　　（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 總結

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

參考文獻

　　[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] 孫全勇.時間自動機及其應用研究[D].哈爾濱：哈爾濱工程大學，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] 陳偉，薛云志，趙琛，等.一種基于時間自動機的實時系統測試方法[J].軟件學報，2007，18（1）：62-73.

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