面向?qū)ο驧SVL語言及其在組合Web服務(wù)驗證中的應(yīng)用.pdf

1、時序邏輯是一種規(guī)范語言，適合于并發(fā)系統(tǒng)的規(guī)范與驗證，已經(jīng)廣泛的應(yīng)用于數(shù)字電路、軟件工程等領(lǐng)域的形式化驗證中。時序邏輯程序設(shè)計語言是時序邏輯的一個可執(zhí)行子集，可以將程序的書寫、性質(zhì)描述和驗證統(tǒng)一在時序邏輯的框架中進行。對軟硬件系統(tǒng)使用時序邏輯程序設(shè)計語言進行建模，對系統(tǒng)期望的性質(zhì)采用時序邏輯公式來描述，將模型和性質(zhì)統(tǒng)一在時序邏輯的框架中，從而實現(xiàn)對軟硬件系統(tǒng)的形式化驗證。 現(xiàn)有的時序邏輯程序設(shè)計語言與傳統(tǒng)的高級程序設(shè)計語言相比，存

2、在形式化程度過高、缺少指針數(shù)據(jù)結(jié)構(gòu)和面向?qū)ο髾C制等不足之處，使用這些語言進行程序設(shè)計較為不便。另外，組合Web服務(wù)的形式化驗證是目前研究的一個熱點，使用時序邏輯程序設(shè)計語言對組合Web服務(wù)進行建模和驗證，能夠?qū)⒛Ｐ秃托再|(zhì)統(tǒng)一在時序邏輯的框架中，給形式化驗證帶來了方便。 本文以框架時序邏輯語言MSVL為研究對象，提出了指針數(shù)據(jù)結(jié)構(gòu)的形式化方法和實現(xiàn)方案，給出了對象、類和繼承等面向?qū)ο蟾拍畹男问交x，并在MSVL解釋器中實現(xiàn)了指針

3、數(shù)據(jù)結(jié)構(gòu)和面向?qū)ο髾C制。為了應(yīng)用MSVL，研究了以O(shè)WL-S為過程描述模型的組合Web服務(wù)，提出了組合Web服務(wù)的基于MSVL的建模方法和驗證方法。 本文的主要貢獻如下： （1）以框架時序邏輯語言MSVL為研究對象，從邏輯語言的角度出發(fā)，提出了基于名字常量的指針形式化方法和實現(xiàn)方案；從命令式語言的角度出發(fā)，提出了基于內(nèi)容變量的指針形式化方法和實現(xiàn)方案。 （2）在MSVL解釋器中實現(xiàn)了基于內(nèi)容變量的指針，使用指針模

4、擬實現(xiàn)了引用調(diào)用的參數(shù)傳遞方式，使用指針實現(xiàn)了原地逆置單鏈表的程序，并使用解釋器對該程序進行了基于模型檢測的形式化驗證。 （3）對投影時序邏輯進行擴展，基于變量集合的層次化和謂詞的分組，給了對象、類和繼承等面向?qū)ο蟾拍畹男问交x，并將擴展投影時序邏輯的一個可執(zhí)行子集定義為面向?qū)ο驧SVL。 （4）提出了面向?qū)ο驧SVL的解釋器基本框架和實現(xiàn)方案，使用VisualC++/Flex/Bison實現(xiàn)了該解釋器；使用面向?qū)ο驧