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

1、隨著軟件復(fù)雜度的不斷增加、應(yīng)用領(lǐng)域的不斷擴(kuò)大，人們對(duì)軟件可靠性的需求日益迫切，如何保證軟件的可靠性成為軟件工程領(lǐng)域的一個(gè)焦點(diǎn)問(wèn)題。傳統(tǒng)的軟件測(cè)試只能發(fā)現(xiàn)錯(cuò)誤，不能保證程序正確。形式化方法被認(rèn)為是解決軟件可靠性的一個(gè)有效途徑，但形式化語(yǔ)言較難掌握，一般開(kāi)發(fā)人員直接書(shū)寫(xiě)比較困難?；诖耍疚奶岢隽艘环N基于規(guī)約模式的、用于描述C程序性質(zhì)的半形式化語(yǔ)言C-PDL，研究了從C-PDL，到模型檢測(cè)工具SPIN輸入語(yǔ)言的轉(zhuǎn)換過(guò)程，最后采用SPIN驗(yàn)證

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

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