1、運(yùn)行時(shí)驗(yàn)證是一種輕量級(jí)的驗(yàn)證技術(shù)，其驗(yàn)證過程伴隨目標(biāo)系統(tǒng)的實(shí)際運(yùn)行。它是傳統(tǒng)驗(yàn)證技術(shù)的有效補(bǔ)充，在許多領(lǐng)域逐漸受到人們的關(guān)注，并被具體運(yùn)用到眾多對(duì)系統(tǒng)安全性有著較高要求的行業(yè)。
　　在運(yùn)行時(shí)驗(yàn)證過程中，針對(duì)需求將待監(jiān)控的性質(zhì)采用某種時(shí)序邏輯進(jìn)行描述，例如用線性時(shí)序邏輯（LTL）公式來描述，再根據(jù)性質(zhì)公式構(gòu)造監(jiān)控器。由于運(yùn)行過程只能觀測到系統(tǒng)的有窮執(zhí)行路徑，因此傳統(tǒng)的運(yùn)行時(shí)驗(yàn)證技術(shù)多是把時(shí)序邏輯的語義改造成為基于有窮路徑的二值語義，

2、這使得使監(jiān)控結(jié)果不能與時(shí)序邏輯性質(zhì)的監(jiān)控需求保持一致，并且在監(jiān)控的預(yù)測性方面存在不足。
　　本文根據(jù)已有的三值語義的監(jiān)控方法，為了便于監(jiān)控器的自動(dòng)生成，基于交錯(cuò)Büchi自動(dòng)機(jī)對(duì)該方法進(jìn)行了改進(jìn)。首先將具有三值語義的LTL公式轉(zhuǎn)化為一個(gè)交錯(cuò)的Büchi自動(dòng)機(jī)，該轉(zhuǎn)換過程的時(shí)空開銷均為線性；接下來，將所得交錯(cuò)Büchi自動(dòng)機(jī)轉(zhuǎn)換為非確定的Büchi自動(dòng)機(jī)；最后將該自動(dòng)機(jī)進(jìn)行確定化，從而得到能夠高效運(yùn)行的監(jiān)控器。
　　本文提出了

3、兩種策略對(duì)Büchi自動(dòng)機(jī)的優(yōu)化：一是通過識(shí)別Büchi自動(dòng)機(jī)中強(qiáng)連通圖，并對(duì)其狀態(tài)進(jìn)行刪除或合并；二是對(duì)Büchi自動(dòng)機(jī)中每一個(gè)狀態(tài)進(jìn)行判空操作，去掉對(duì)應(yīng)語言為空的狀態(tài)。通過這樣的優(yōu)化，有效的降低了所生成監(jiān)控器的規(guī)模。
　　以上述方法為基礎(chǔ)，本文對(duì)JavaMOP監(jiān)控工具進(jìn)行擴(kuò)展，使其能夠支持三值LTL監(jiān)控器的生成，并在美國航空航天局（NASA）的“火星車仿真軟件 Maestro”以及某“月球巡視器”系統(tǒng)中進(jìn)行了實(shí)驗(yàn)，取得了良好效