基于規(guī)約模式的C程序性質描述與驗證.pdf

1、隨著軟件復雜度的不斷增加、應用領域的不斷擴大，人們對軟件可靠性的需求日益迫切，如何保證軟件的可靠性成為軟件工程領域的一個焦點問題。傳統(tǒng)的軟件測試只能發(fā)現(xiàn)錯誤，不能保證程序正確。形式化方法被認為是解決軟件可靠性的一個有效途徑，但形式化語言較難掌握，一般開發(fā)人員直接書寫比較困難。基于此，本文提出了一種基于規(guī)約模式的、用于描述C程序性質的半形式化語言C-PDL，研究了從C-PDL，到模型檢測工具SPIN輸入語言的轉換過程，最后采用SPIN驗證

2、C程序是否滿足C-PDL，描述的性質。 規(guī)約模式是根據(jù)常用時序邏輯公式抽象而成的一種半形式化表達模式，用其描述的性質有對應的LTL表達式。現(xiàn)有規(guī)約模式的語義較含糊，導致用其描述的性質可以對應不同的LTL表達式，目前有SPS和Prospcc兩種版本。本文以SPS為標準，基于SPIN工具驗證LTL，表達式，并根據(jù)驗證結果糾正了規(guī)約模式的語義，保證了它們的一致。 C程序描述的是一系列狀態(tài)轉換的過程，可以引入規(guī)約模式描述程序性質

3、。為了能更直觀地表達程序性質以及準確地找到錯誤路徑，本文對傳統(tǒng)的狀態(tài)進行擴展，使其不僅包含變量的取值，還包含位置信息，通過位置信息可以定位到具體的代碼行。本文提出的C-PDL是描述C程序性質的半形式化語言，以規(guī)約模式為基礎、以擴展后的狀態(tài)為組成元素，并增加了描述斷言的表達模式，能夠描述順序程序和并發(fā)程序的動態(tài)性質及程序的不變量。由于SPIN不能直接驗證C-PDL描述的性質，本文研究了從C-PDL到SPIN輸入語言的轉換過程。 在