面向對象MSVL語言及其在組合Web服務驗證中的應用.pdf

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

2、在形式化程度過高、缺少指針數(shù)據(jù)結構和面向對象機制等不足之處，使用這些語言進行程序設計較為不便。另外，組合Web服務的形式化驗證是目前研究的一個熱點，使用時序邏輯程序設計語言對組合Web服務進行建模和驗證，能夠將模型和性質統(tǒng)一在時序邏輯的框架中，給形式化驗證帶來了方便。 本文以框架時序邏輯語言MSVL為研究對象，提出了指針數(shù)據(jù)結構的形式化方法和實現(xiàn)方案，給出了對象、類和繼承等面向對象概念的形式化定義，并在MSVL解釋器中實現(xiàn)了指針

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

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