概率時段演算的模型檢驗概述

吳敏

摘要：在實際工程應用中，越來越多的系統表現出具有概率性等特征。作為對于此類實時系統的建模，概率時間自動機因為其能同時表示概率性、隨機性和不確定性而被廣泛采用。在對此類帶概率性質的實時系統進行描述時，作為時段演算的一種擴展，概率時段演算被用來計算此類系統滿足需求的概率。該文主要概述基于概率時間自動機的概率時段演算的模型檢驗主要步驟及其核心算法，其中模型檢驗的核心算法通過分別將前兩者轉換為區域圖和概率分支時間邏輯來達成。

關鍵詞：實時系統；模型檢驗；概率時間自動機；概率時段演算

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

1 背景

隨著互聯網的快速發展，軟件系統日趨復雜，軟件的可靠性、安全性等問題越加突出，潛在的錯誤可能引發災難性的后果。因此，如何確保軟件系統的正確性和可靠性，并及時發現系統中的錯誤至關重要。在這方面，形式化驗證方法起到了重要作用。

帶概率時間自動機以及相關性質的模型檢驗在工程上具有重要的意義。它保證了實際應用中相關具有概率性為系統例如媒體設備、通信協議等的可靠性、安全性，用于驗證具有概率隨機行為的系統中事件發生的概率，如“某段時間內，系統出錯的概率小于0.05%”、“相應時間內，發送者收到確認的概率大于99.99%”等性質。對于帶概率的實時系統的建模，由于概率時間自動機能同時表示概率性、隨機性和不確定性，因而在實際中有廣泛應用。……