[發明專利]一種運行時驗證中性質的可監控性概率的度量方法

有效

• 申請號: 202010157636.2
• 申請日: 2020-03-09
• 公開（公告）號: CN111352848B
• 公開（公告）日: 2021-07-20
• 發明（設計）人: 陳哲;陳云云;吳逸凡
• 申請（專利權）人: 南京航空航天大學
• 主分類號: G06F11/36
• 分類號: G06F11/36;G06F11/30
• 代理公司: 南京經緯專利商標代理有限公司 32200
• 代理人: 施昊

本發明公開了一種運行時驗證中性質的可監控性概率的度量方法，首先將性質轉化為對應的監控器，然后將監控器轉換為對應的離散時間馬爾可夫鏈，最后列出關于可監控有限序列概率的線性方程組，并通過對該方程組進行求解，得到最終的可監控性概率。相比于已有技術，本發明不再簡單地通過可監控性或弱可監控性來判斷給定性質在運行時驗證中的適用性，而是通過計算可監控性概率，使得程序開發人員和驗證工程師可以在進行運行時驗證之前，更加準確地判斷性質被驗證的價值大小，從而提高軟件驗證的效率和質量。

技術領域

本發明屬于計算機軟件領域，尤其是指運行時驗證領域。

背景技術

隨著信息和計算機技術的迅猛發展，計算機軟件在當今社會的各個領域都發揮著越來越重要的作用。與此同時，軟件缺陷所造成的后果也越來越不可忽視。在醫療、航空、航天及國防軟件中，一個錯誤可能導致不可估量的損失。例如：Therac-25放射治療儀的軟件設計缺陷導致重大醫療事故，六位病人因此高度灼傷甚至死亡；阿麗亞娜5號火箭升空后的爆炸導致了近85億美元損失，其原因是系統軟件試圖將一個64位的數字塞入16位的空間產生的溢出錯誤。鑒于此，軟件的安全性和可靠性越來越受到人們的關注和重視。

運行時驗證是一種輕量級的形式化驗證技術，用于確保軟件的安全性和可靠性。該技術自動地將程序需要滿足的性質合成為監控器，監控器通過在運行時監測程序的行為來檢查其是否滿足或違反給定的性質，以此來驗證程序的正確性或者發現程序中的錯誤。此外，還可以在發現錯誤時發出警告或進行錯誤恢復。運行時驗證通常使用線性時序邏輯、針對有限或無限長度執行序列的有限狀態機和正則表達式等形式化語言來描述程序需要滿足的性質。

然而，并不是所有的性質都適合用于運行時驗證。因此，人們用可監控性和弱可監控性來衡量一個性質在運行時驗證中的適用性。其中，一個性質是可監控的，當且僅當程序所有的有限長度執行序列都能通過有限步的擴展來滿足或者違反該性質，即所有的有限執行序列都是可監控的；一個性質是弱可監控的，當且僅當至少存在一條程序的有限長度執行序列滿足或者違反該性質，即至少存在一條有限執行序列是可監控的。由此可見，可監控性的要求過于嚴格，因為它要求“所有的”執行序列都是可監控的；而弱可監控性的要求過于寬松，因為它僅要求“存在”可監控的執行序列，無論是一條、多條還是所有序列。而對于處于二者之間(即弱可監控但不可監控)的性質，人們無法對這些性質可監控的程度進行度量。

研究發現，不同性質的可監控有限序列的數量占所有可能有限序列的數量的比例是不一樣的。一個性質的可監控有限序列所占的比例越大，那么該性質在運行時驗證中就越有可能給出確定的判定結果，其被驗證的價值也就越大。但是，現有的可監控性和弱可監控性無法度量這個比例。例如，可監控性要求所有的有限序列都是可監控的，即比例為100％；而弱可監控性要求性質存在可監控的部分即可，即比例大于0，但無法量化具體的比例數值。因此，為了準確地度量給定性質在運行時驗證中的價值大小，為程序開發人員和驗證工程師提供量化的價值參考，亟待提出一種能夠度量性質的可監控性概率的方法。

發明內容

為了克服上述背景技術提到的技術問題，本發明提出了一種運行時驗證中性質的可監控性概率的度量方法。

一種運行時驗證中性質的可監控性概率的度量方法，包括以下步驟：

(1)將給定的性質轉化為對應的監控器

(2)遍歷監控器獲取的初始狀態、遷移上的標簽公式、不可監控狀態集合U和不可監控狀態集合的前驅狀態集合

(3)根據不可監控狀態集合U判斷是否提前返回性質的可監控性概率結果；

(4)將監控器轉換為對應的離散時間馬爾可夫鏈

(5)根據監控器的不可監控狀態集合U、不可監控狀態集合的前驅狀態集合以及離散時間馬爾可夫鏈的遷移概率分布函數和初始概率分布函數，列出關于可監控性概率的線性方程組E；