[發明專利]一種線性時態邏輯規范的通用并行挖掘方法

在審

• 申請號: 201710139684.7
• 申請日: 2017-03-09
• 公開（公告）號: CN106886417A
• 公開（公告）日: 2017-06-23
• 發明（設計）人: 何積豐;熊家文;史建琦;黃滟鴻;李昂;方徽星
• 申請（專利權）人: 華東師范大學;上海豐蕾信息科技有限公司
• 主分類號: G06F9/44
• 分類號: G06F9/44
• 代理公司: 北京辰權知識產權代理有限公司11619
• 代理人: 郎志濤

技術領域

本發明涉及一種計算機技術領域，尤其是模型檢測領域中的線性時態邏輯的規范挖掘技術，具體涉及一種線性時態邏輯規范的通用并行挖掘方法。

背景技術

與其他工程產品不同的是，軟件產品在其整個生命周期中會不斷地變化演進。而在對軟件進行維護、更新的過程中，為保持系統原有功能的正確性，維護人員通常需要付出極大的努力。據統計，軟件的維護成本占據了軟件開發成本的90％。因此，研究如何降低軟件維護成本具有十分現實的意義。

而軟件維護成本之中的絕大部分，都源于對遺留源代碼理解吸收所產生的成本。有研究表明，為理解原有代碼付出的代價超過了總維護代價的50％。通常，開發人員會選擇閱讀軟件規范文檔來輔助軟件程序的理解。然而，在許多企業中，開發人員迫于市場應用的時效性，疏忽了規范文檔的編寫與維護，以至于很大部分的軟件規范文檔并沒有隨著軟件程序的演化得到及時的更新。這樣，經過若干次演化周期，最新版本的軟件程序早就與原始的規范文檔大相徑庭。因此，如何及時地更新軟件規范，成為了一個值得探索的問題。

另外，為了保證軟件系統的正確性，人們提出了模型檢測技術。例如申請號為201510395404.X，發明名稱為安全交換協議模型檢測方法的中國發明專利，公開了一種安全交換協議模型檢測方法，該方法的步驟包括：1)構建安全交換協議模型；2)構建安全屬性模型；3)構建攻擊者模型；4)狀態約簡以及模型檢測。

模型檢測技術主要通過對軟件系統進行抽象建模，并采用一系列的形式化性質來驗證模型是否符合特定性質，以研究系統是否具有某種性質，或違反某種約束。線性時態邏輯通常用于形式化定義模型所該具備的性質和約束。然而，構造形式化性質的困難一直阻礙了模型檢測技術的廣泛應用。

因此，有必要尋找一種方法，能夠自動地從軟件系統中獲取軟件系統具備的性質或約束。正如人們觀察自然現象來了解自然規律，可以采用某種自動化的方法，根據軟件系統的運行日志，運行軌跡來學習、挖掘軟件系統所具備的性質。

發明內容

為解決以上問題，本發明公開了一種線性時態邏輯規范的通用并行挖掘方法，主要用于從軟件系統的日志文件中挖掘日志中各種事件之間所具備的線性時序關系，用于獲取日志中事件之間的規律，以推測出軟件程序中可能具備的線性時態性質，從而輔助對程序的理解分析，也可用于通信協議分析。

具體的，本發明公開了一種線性時態邏輯規范的通用并行挖掘方法，包括如下步驟：

預處理步驟，對日志文件進行分割，分離出日志文件中的獨立軌跡，獲取日志文件中所有事件的集合以及每個事件在獨立軌跡中出現的位置；

規范實例生成步驟，根據輸入的規范模板集合，將其中的變量與日志事件集合中的事件依次進行綁定，以獲取規范實例候選集合；

規范實例驗證步驟，依次對規范實例候選集合中的規范實例進行驗證，計算其在日志中的支持度、置信度情況；

結果篩選步驟，根據輸入的挖掘要求，從規范實例候選集合中去除支持度、置信度不符合要求的規范實例。

優選的，如上所述的線性時態邏輯規范的通用并行挖掘方法，所述預處理步驟包括如下子步驟：

軌跡分離步驟，通過文本處理，將日志中的數據讀取到內存中，按照分隔符進行分離，獲取一個元素為單條軌跡所組成的集合；

事件集合獲取步驟，分別掃描每條軌跡，以上述分隔符對軌跡進行分割處理，獲取原子事件集合；

事件位置信息獲取步驟，掃描每條軌跡，記錄事件在軌跡中出現的位置信息。

優選的，如上所述的線性時態邏輯規范的通用并行挖掘方法，所述預處理步驟的實現過程為：順序地從日志文件中讀取字符串，在遇到分隔符時，識別并判斷該分隔符為事件分隔符或者是軌跡分隔符，若為軌跡分隔符，則當前軌跡終止并新建一個軌跡存儲對象；若為事件分隔符，則記錄新的事件位置信息，并將該事件加入到事件集合之中。

優選的，如上所述的線性時態邏輯規范的通用并行挖掘方法，所述規范實例生成步驟包括如下三個子步驟：

規范模板分析步驟，對輸入的規范模板進行語法分析，獲取規范模板中的變量；

變量綁定步驟，用事件集合中的事件，對規范模板中的變量進行替換，即將規范模板中的變量綁定為特定的事件；

實例生成步驟，規范模板中的變量都綁定事件后，則成為一個具體的規范實例，不同規范模板變量綁定不同的事件，以生成不同的規范實例。

優選的，如上所述的線性時態邏輯規范的通用并行挖掘方法，所述規范實例驗證步驟包括如下三個子步驟：