概率線性時段不變式的統計模型檢驗

摘要：模型檢驗是軟件工程形式化方法的一個重要組成部分，線性時段不變式是形式化方法中表述系統性質的一種重要表達式。對線性時段不變式的模型檢驗一直是形式化方法研究的一個重要內容。該文提出了一種針對帶概率的線性時段不變式的模型檢驗方法，該方法針對不帶有不確定性的概率模型，運用統計模型檢驗的方法，基于UPPAAL工具實現了概率線性時段不變式的統計模型檢驗。

關鍵詞：模型檢驗；時段驗算；UPPAAL；概率線性時段不變式

中圖分類號：TP311 文獻標識碼：A 文章編號：1009-3044（2014）30-7097-03

隨著計算機技術的飛速發展，計算機系統的規模和復雜性急劇增加，系統出錯的概率隨之增大。在一些重要的實時系統中，如航空交管、核電站監控等，任何錯誤都可能造成重大的經濟損失和人員傷亡。如何在系統開發早期階段驗證設計的正確性，成為研究人員面對的重要問題。形式化方法（Formal Methods）是重要的提高系統可靠性和安全性的方法。模型檢驗（Model Checking）是形式化方法的重要組成部分。它是一種自動驗證有窮狀態系統的技術，通過窮舉搜索狀態空間來判斷系統是否滿足規約。時段驗算（Duration Calculus）[1]是周巢塵院士提出的一種區間時態邏輯，用于描述系統的區間性質。線性時段不變式是時段驗算性質的子集。

本文提出了對于一些概率系統，針對由概率線性時段不變式描述的系統性質的統計模型檢驗方法。該方法主要基于模型檢驗工具UPPAAL完成。主要思想是將概率線性時段不變式轉化成概率計算樹邏輯（Probabilistic Computing Tree Logic）[2]，然后由UPPAAL完成模型檢驗。……