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

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

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

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