[發明專利]一種面向完全正則時序邏輯性質的高效運行時監控方法在審
| 申請號： | 202210974710.9 | 申請日： | 2022-08-15 |
| 公開（公告）號： | CN116107862A | 公開（公告）日： | 2023-05-12 |
| 發明（設計）人： | 于斌;董彥松;田聰;段振華;王小兵;陸旭;張南;趙亮 | 申請（專利權）人： | 西安電子科技大學 |
| 主分類號： | G06F11/36 | 分類號： | G06F11/36 |
| 代理公司： | 西安嘉思特知識產權代理事務所(普通合伙) 61230 | 代理人： | 李薇 |
| 地址： | 710071*** | 國省代碼： | 陜西;61 |
| 權利要求書： | 查看更多 | 說明書： | 查看更多 |
| 摘要： | |||
| 搜索關鍵詞： | 一種 面向 完全 正則 時序 邏輯 性質 高效 運行 監控 方法 | ||
1.一種面向完全正則時序邏輯性質的高效運行時監控方法，其特征在于，包括：
采用MSVL語言編寫待監控程序，得到MSVL程序；
采用PPTL公式形式化描述待驗證的時序邏輯性質；
針對PPTL公式中涉及的與MSVL程序有關的程序變量，對MSVL程序進行插樁；
根據所述MSVL程序在動態執行過程中生成的狀態序列，檢測所述MSVL程序的實時運行狀態，并根據檢測結果判斷MSVL程序的運行狀態是否滿足所述待驗證的時序邏輯性質。
2.根據權利要求1所述的面向完全正則時序邏輯性質的高效運行時監控方法，其特征在于，所述采用MSVL語言編寫待監控程序，得到MSVL程序的步驟，包括：
采用MSVL語言編寫所述待監控程序中的順序語句、分支語句和循環語句，得到MSVL程序。
3.根據權利要求1所述的面向完全正則時序邏輯性質的高效運行時監控方法，其特征在于，所述待驗證的時序邏輯性質包括：安全性、活性、弱公平性和周期重復性。
4.根據權利要求1所述的面向完全正則時序邏輯性質的高效運行時監控方法，其特征在于，所述針對PPTL公式中涉及的與MSVL程序有關的程序變量，對MSVL程序進行插樁的步驟，包括：
確定PPTL公式中涉及的MSVL程序變量；
在對MSVL程序靜態分析的階段，當所述程序變量作為賦值語句的左值時，在所述賦值語句后進行程序插樁，獲得MSVL程序動態執行過程中該程序變量的取值。
5.根據權利要求4所述的面向完全正則時序邏輯性質的高效運行時監控方法，其特征在于，所述根據所述MSVL程序在動態執行過程中生成的狀態序列，檢測所述MSVL程序的實時運行狀態，并根據檢測結果判斷MSVL程序的運行狀態是否滿足所述待驗證的時序邏輯性質的步驟，包括：
獲取所述MSVL程序動態執行過程中根據所述程序變量的取值生成的狀態序列，并將所述狀態序列劃分為多個子序列；
利用調度線程將多個驗證任務分配至分布式設備，以使所述分布式設備同時檢測所述多個子序列；其中，所述多個驗證任務與所述多個子序列一一對應；
對驗證結果進行匯總，并判斷MSVL程序的運行狀態是否滿足待驗證的性質。
6.一種面向完全正則時序邏輯性質的高效運行時監控裝置，其特征在于，包括：
編寫模塊，用于采用MSVL語言編寫待監控程序，得到MSVL程序；
描述模塊，用于采用PPTL公式形式化描述待驗證的時序邏輯性質；
插樁模塊，用于針對PPTL公式中涉及的與MSVL程序有關的程序變量，對MSVL程序進行插樁；
檢測模塊，用于根據所述MSVL程序在動態執行過程中生成的狀態序列，檢測所述MSVL程序的實時運行狀態，并根據檢測結果判斷MSVL程序的運行狀態是否滿足所述待驗證的時序邏輯性質。
7.一種電子設備，其特征在于，包括處理器、通信接口、存儲器和通信總線，其中，處理器，通信接口，存儲器通過通信總線完成相互間的通信；
存儲器，用于存放計算機程序；
處理器，用于執行存儲器上所存放的程序時，實現權利要求1-5任一所述的方法步驟。
8.一種計算機可讀存儲介質，其特征在于，所述計算機可讀存儲介質內存儲有計算機程序，所述計算機程序被處理器執行時實現權利要求1-5任一所述的方法步驟。
該專利技術資料僅供研究查看技術是否侵權等信息，商用須獲得專利權人授權。該專利全部權利屬于西安電子科技大學，未經西安電子科技大學許可，擅自商用是侵權行為。如果您想購買此專利、獲得商業授權和技術合作，請聯系【客服】
本文鏈接：http://www.szxzyx.cn/pat/books/202210974710.9/1.html，轉載請聲明來源鉆瓜專利網。
