[發明專利]一種基于定量驗證方法的并發實時系統可靠性評估方法

有效

• 申請號: 201711456212.0
• 申請日: 2017-12-28
• 公開（公告）號: CN108052768B
• 公開（公告）日: 2021-06-25
• 發明（設計）人: 王曉燕;于海;劉淑芬
• 申請（專利權）人: 吉林大學
• 主分類號: G06F30/20
• 分類號: G06F30/20;G06F119/02;G06F111/04;G06F111/08
• 代理公司: 長春市盈創中成知識產權代理事務所(普通合伙) 22215
• 代理人: 季建文

本發明公開了一種基于定量驗證方法的并發實時系統可靠性評估方法，其包括以下步驟：(1)采用帶參數的概率時間接口自動機構建并發實時系統模型；(2)對步驟(1)中建立的模型按照接口上的輸入/輸出動作對進行組合，并使用帶參數的前向可達性算法將組合后的PPTIA模型轉換成為時域圖；(3)使用概率時間邏輯語言PTSL構建可靠性要求的形式化規約；(4)使用驗證算法評估并發實時系統的可靠性。本發明針對現有邏輯語言無法直接將策略進行形式化表示的不足以及在設計階段無法精確獲取模型所需要的數據問題，采用基于帶參數的概率時間接口自動機和概率時間策略邏輯的定量驗證方法來評估并發實時系統的可靠性。

技術領域

本發明屬于計算機應用技術領域，主要涉及形式化驗證技術，具體是一種基于定量驗證方法的并發實時系統可靠性評估方法。

背景技術

隨著計算機技術的飛速發展，計算機系統的規模越來越大、復雜性也日趨增加，要保證系統的可靠性、安全性越來越困難，且由于這些系統通常具有交互、實時、并發、分布等特征，因此其行為具有一定的不確定性，這也造成傳統的測試方法如跟蹤調試、用例覆蓋等技術難以達到理想的測試效果。因此如何保證系統的正確性和可靠性成為日益緊迫的問題。在為此提出的諸多理論和方法中，模型檢測(model checking)以其簡潔明了和自動化程度高而引人注目。1981年，Clarke和Emerson提出了描述并發系統性質的時序邏輯CTL(Computation Tree Logic，計算樹邏輯)，以及檢查有窮狀態并發系統是否滿足CTL公式的算法，開創了模型檢測這一研究方向。現在模型檢測已被應用于計算機硬件、軟件、通信協議、控制系統、安全認證協議等領域，取得了令人矚目的成功，成為分析、驗證復雜系統的最重要的技術，并被Intel、IBM、微軟等公司用于生產實踐中。模型檢測的基本思想是用狀態遷移系統表示系統的行為，用時序邏輯公式描述系統的性質，這樣系統是否具有所期望的性質就轉化為數學問題“狀態遷移系統是否是公式的一個模型”。模型檢測作為形式化驗證的一種主流技術，可以克服傳統軟件測試用例生成不完備的不足,同時具有驗證自動化的優點，并且當驗證的性質不滿足時，能給出違背性質的反例。由于模型檢測采用了嚴格的形式化方法對系統進行驗證，因此比測試和仿真更能保證系統的正確性。定量驗證技術與傳統的非概率的模型驗證技術的不同在于除了需要對模型的狀態進行遍歷外，還需要進行大量的數值計算。隨著并發實時系統越來越多的應用在一些對安全性、可靠性要求非常高的領域，如航空系統、電力系統、智能交通系統、網絡防御系統等，系統發生故障所帶來的后果越來越嚴重，因此使用定量驗證技術對并發實時系統中的可靠性進行分析是非常必要的。

在分析并發實時系統時，分析人員常使用術語--策略來描述滿足特定條件的解決方案，然而在定量驗證中，分析人員無法直接將策略進行形式化表達，而只能使用PCTL，ATL等的形式化邏輯語言來表達可到達的狀態節點及其概率，因此分析人員必須將策略轉換成PCTL等邏輯語言能夠表達的等價形式，增加了分析人員的負擔。因此本發明使用概率時間策略邏輯(Probabilistic Timed Strategy Logic，PTSL)語言，把策略作為第一實體對象，能夠針對每個agent對象所使用的策略進行描述，從而使我們能夠以簡單而自然的方式指定并發實時系統中的可靠性屬性。

另外目前的定量驗證方法雖然可以計算出滿足某一個特性的最大/最小概率，但是在定量驗證過程中，模型中使用的數據在早期設計階段往往是很難獲得的，而且整個系統的環境也是未知的，這就給定量驗證結果的正確性帶來問題。本發明使用帶參數的概率時間接口自動機，將參數引入模型，在驗證過程中通過算法能夠自動的找到滿足某個性質的參數值以及最優解。當參數的某個值不滿足所要驗證的性質時，可以重新定義參數值，直到找到最優解。

發明內容

本發明針對現有邏輯語言無法直接將策略進行形式化表達的不足以及在設計階段無法精確獲取模型所需要的數據問題，提出了一種基于帶參數的概率時間接口自動機和概率時間策略邏輯的定量驗證方法，并將其用來評估并發實時系統的可靠性。

為了解決上述技術問題，本發明提供了如下的技術方案：