基于運行時驗證的監(jiān)控器生成技術(shù)研究.pdf

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

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

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