實時系統(tǒng)的測試方法研究與應(yīng)用.pdf

1、隨著計算機與互聯(lián)網(wǎng)的迅速普及，實時系統(tǒng)在各個領(lǐng)域都得到了廣泛的應(yīng)用，該類系統(tǒng)諸多動作的實現(xiàn)與時間息息相關(guān)，都需要滿足一定的時間約束。因此，對這類系統(tǒng)的可靠性與安全性的問題得到了研究人員的廣泛關(guān)注?；谀Ｐ偷臋z測方法是一種對實時系統(tǒng)檢測和驗證的常用方法，其中時間自動機是諸多模型中使用最為廣泛的一種建模工具，它是對自動機理論的擴展，具有描述方法簡潔和描述能力強等特點，因而作為模擬實時系統(tǒng)行為的模型得到廣泛的研究與應(yīng)用。
　　本文基于的

2、是時間自動機模型對實時系統(tǒng)進(jìn)行建模，主要工作如下:
　　(1)在時鐘區(qū)域劃分方法的基礎(chǔ)上，提出一種新的劃分方法，將無窮狀態(tài)空間的時鐘區(qū)域在時鐘數(shù)量對應(yīng)的坐標(biāo)圖中劃分為若干個等價類，其中只劃分為相關(guān)的區(qū)域內(nèi)和區(qū)域外的兩種類型，使得用最少的點能夠等價的對應(yīng)更多的狀態(tài)空間，簡化了對每一個時鐘空間的選取，進(jìn)而減少測試用例的生成數(shù)量。同時，還提出了新的計算區(qū)域數(shù)量的方法以及對時鐘區(qū)域?qū)?yīng)區(qū)間與時鐘約束的轉(zhuǎn)換進(jìn)行了分析總結(jié)，并得出一般的公式。

3、
　　(2)針對時間自動機的執(zhí)行狀態(tài)空間的爆炸問題，特別是其執(zhí)行模擬空間存在無窮狀態(tài)，采用基于抽象約簡的方法對執(zhí)行狀態(tài)空間約簡。該抽象約簡的技術(shù)可以在可達(dá)性和安全性上與原系統(tǒng)保持模擬或互模擬關(guān)系，并能夠?qū)o窮的狀態(tài)空間約簡為有限的狀態(tài)空間同時保持相應(yīng)的屬性，進(jìn)一步約簡原狀態(tài)空間測試用例的數(shù)目和長度，最終實現(xiàn)了測試用例的約簡。
　　(3)針對執(zhí)行狀態(tài)中時間約束表達(dá)式的冗余和無解問題，采用基于有界差分矩陣(DBM)的表達(dá)式約簡技