基于模型檢測的軟件可靠性驗證方法.pdf

1、隨著信息技術的快速發(fā)展，計算機軟件的應用領域不斷擴大，其功能和規(guī)模也日益復雜。這些軟件系統(tǒng)運行時如果出現(xiàn)故障，將造成不可估量的損失。如何有效保證軟件系統(tǒng)的可靠性，成為一個十分緊迫而且嚴峻的問題。模型檢測作為一種重要的形式化驗證技術，已逐漸應用于軟件可靠性驗證中。本課題基于模型檢測技術，重點針對復雜軟件建模困難、狀態(tài)空間爆炸等實際問題，對軟件可靠性驗證方法展開研究。
　　首先，將模型檢測技術用于軟件系統(tǒng)設計階段。提出了一種基于狀態(tài)變

2、遷矩陣的軟件設計建模方法，闡述了其形式化定義和動態(tài)行為描述方法。并引入時間和概率因子對狀態(tài)變遷矩陣模型進行擴展，以解決具有實時特性和隨機行為特性的復雜軟件系統(tǒng)建模困難問題?；跀U展的時間狀態(tài)變遷矩陣模型，提出了實時軟件設計驗證的符號化編碼方法和性質描述方法，并采用限界模型檢測技術和可滿足性模理論進行設計規(guī)范驗證。實驗結果證明了該方法在軟件設計可靠性驗證方面的有效性。
　　其次，將模型檢測技術用于代碼開發(fā)階段。提出了一種基于程序骨架