并發(fā)系統(tǒng)中基于偏序規(guī)約的狀態(tài)空間約簡與應用.pdf

1、隨著人們對軟硬件系統(tǒng)功能需求的日益增加，導致系統(tǒng)的規(guī)模越來越復雜，其安全性和可靠性也越來越難以得到保證。在一些關鍵領域，例如航空航天、銀行、證券等，軟件可靠性問題顯得尤為重要，已經(jīng)日益成為當今研究的重要課題。在過去的三十幾年間，針對并發(fā)系統(tǒng)運行的不確定性，各國研究人員為解決可靠性問題做出了許多工作，其中，模型檢測驗證技術就是該領域中的熱點之一。
　　模型檢測是一種形式化自動驗證技術，它可以為許多軟件設計中的相關問題提出解決辦法。一

2、般給定一個系統(tǒng)的形式化數(shù)學模型以及形式化的規(guī)約屬性，就可以使用模型檢測技術驗證該系統(tǒng)是否滿足屬性。自動檢測器的檢測結果要不證明該系統(tǒng)滿足該屬性，要不提供一個反例路徑。然而，對于許多類型的系統(tǒng)來說，隨著建模系統(tǒng)規(guī)模和進程數(shù)目的擴大，運行過程中可能產生的狀態(tài)數(shù)將呈指數(shù)級增長，這就引起了狀態(tài)爆炸問題。
　　偏序規(guī)約技術就是為了緩解異步并發(fā)系統(tǒng)的狀態(tài)爆炸問題而產生的，該技術主要是構建一個更小的狀態(tài)空間子集，而搜索時僅探測該狀態(tài)空間子集，并

3、不是探測所有的并發(fā)交錯運行。
　　本文中，我們對模型檢測技術和偏序規(guī)約技術進行深入的研究，主要工作如下：
　　1、詳述了并發(fā)系統(tǒng)的形式化描述方法及模型檢測的一些基本原則，并研究如何使用TLA+語言對現(xiàn)實問題進行規(guī)約。
　　2、研究了偏序規(guī)約的相關理論，同時對幾種約簡狀態(tài)空間的偏序規(guī)約算法進行深入研究，包括充足集(ample)、持久集(persistent)、條件頑固集（conditional stubborn）。