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

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

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

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