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

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

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

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