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

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

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

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

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