[發明專利]一種基于Büchi自動機化簡運行時驗證監控器的方法

在審

• 申請號: 201811359544.1
• 申請日: 2018-11-15
• 公開（公告）號: CN109522713A
• 公開（公告）日: 2019-03-26
• 發明（設計）人: 錢俊彥;葉玲玲
• 申請（專利權）人: 桂林電子科技大學
• 主分類號: G06F21/52
• 分類號: G06F21/52;G06F9/448
• 代理公司: 桂林市持衡專利商標事務所有限公司 45107
• 代理人: 陳躍琳

本發明公開一種基于Büchi自動機化簡運行時驗證監控器的方法，首先將LTL公式描述的屬性轉化為Büchi自動機；接著對Büchi自動機的狀態進行冗余標記和移除；之后在Büchi自動機中尋找互相滿足公平模擬關系的狀態對，并對狀態對進行合并；最后將化簡后的Büchi自動機轉化成確定性有限狀態自動機，得到用于驗證的監控器。本發明能夠加速Büchi自動機到確定性有限狀態自動機的轉換，同時使JavaMop工具進行驗證時的內存開銷得到減少。

技術領域

本發明涉及運行時驗證技術領域，具體涉及一種基于Büchi自動機化簡運行時驗證監控器的方法。

背景技術

運行時驗證(RV)是一種基于系統運行狀態來檢測異常發生的技術，其能夠對正在運行的系統進行實時監控，一旦發現系統的行為違反某些屬性規則，就會立即給予提醒或作出反應。在進行運行時驗證時，監控器是對被驗證系統進行檢測的模塊，它接收系統的運行蹤跡，然后根據給定的屬性，對系統行為是否滿足給定屬性進行檢查判斷，并給出一個結論。監控器在運行時驗證過程中有著重要的作用，它的運行效率影響著整個系統驗證的效率。

目前，監控器的構造方法有多種，其中基于自動機的監控器構造技術較為常見。Büchi自動機是ω-自動機的一種，它將有限狀態自動機擴展為能接受無限輸入的自動機，即接受一個無限輸入序列的自動機。Büchi自動機是一個很好的替代和處理ω正則語言的方式，因為它們在布爾操作下是封閉的，所以它常被用在基于自動機的形式化驗證方法中。在運行時驗證中，使用時態邏輯描述的屬性經常被轉換成確定化的有窮狀態自動機，Büchi自動機在這個轉換過程中被作為一個中間的媒介。然而，在這一轉換過程中自動機的狀態和遷移關系的數量非常大，會消耗大量的內存和時間，這有待進一步的化簡改進。

發明內容

本發明所要解決的是現有運行時驗證工具JavaMOP中以Büchi自動機為基礎進行驗證時所存在的較大開銷問題，提供一種基于Büchi自動機化簡運行時驗證監控器的方法，其能夠化簡轉換過程中的狀態和遷移關系，減小監控開銷。

為解決上述問題，本發明是通過以下技術方案實現的：

一種基于Büchi自動機化簡運行時驗證監控器的方法，其具體包括步驟如下：

步驟1、將線性時態邏輯公式描述的屬性轉換為非確定Büchi自動機；

步驟2、對于步驟2所得到的非確定Büchi自動機的狀態集合中的每個狀態，判斷以該狀態開始時，非確定Büchi自動機接受的語言是否為空：若為空，則對該狀態進行冗余標記；否則，該狀態不作標記；

步驟3、將步驟2所得到的有冗余標記的狀態從非確定Büchi自動機的狀態集合中刪除，得到初步簡化的非確定Büchi自動機；

步驟4、在步驟3所得到的初步簡化的非確定Büchi自動機中尋找互相滿足公平模擬關系的狀態對；

步驟5、對步驟4所得到的狀態對進行合并，得到最終簡化的非確定Büchi自動機；

步驟6、將步驟5所得到的最終簡化的非確定Büchi自動機轉化成非確定有限狀態自動機，再對非確定有限狀態自動機進行確定化后，得到確定性有限狀態自動機；

步驟7、將步驟6所得到的確定性有限狀態自動機作用于系統驗證的監控器。

上述步驟1的具體過程如下：首先，將線性時態邏輯公式描述的屬性轉化為交錯自動機；接著，將交錯自動機轉化成廣義的Büchi自動機；最后，把廣義的Büchi自動機轉化為非確定Büchi自動機。

上述步驟5在進行狀態對的合并時，需要檢查合并狀態對后是否會改變初步簡化的非確定Büchi自動機接受的語言：如果接受的語言沒有改變，則對該對狀態對進行合并，并移除合并后多余的轉移關系；否則，不進行狀態對的合并。