框架時序邏輯程序語言MSVL的形式語義.pdf

1、形式語義是對軟件系統(tǒng)進行形式化驗證和分析的重要理論基礎。程序語言的語義可以幫助人們更好的理解、執(zhí)行、分析軟件系統(tǒng)。操作語義有助于語言的實現(xiàn)，公理語義有利于程序的驗證，指稱語義在強大的數學理論支持下為程序的含義提供了精確的數學描述。 時序邏輯程序設計是一種新型的程序設計范式，程序的具體執(zhí)行和性質的描述可以在同一邏輯框架內表示，適用于并發(fā)系統(tǒng)的建模、模擬和驗證。盡管研究人員開發(fā)了相關的解釋器來執(zhí)行各類時序邏輯程序語言，時序邏輯及其可

2、執(zhí)行子集被廣泛地應用于系統(tǒng)的規(guī)范和驗證中，但是到目前為止，至少在區(qū)間時序邏輯程序語言中，還沒有一套系統(tǒng)而完整的形式語義。本文以區(qū)間時序邏輯程序語言MSVL為研究對象，分別從模型語義、操作語義、公理語義三條主線來研究區(qū)間時序邏輯程序的形式語義，并對三種語義之間的一致性、互補性進行分析和證明。 本文研究了MSVL語言的極小模型語義。由于MSVL語言中的框架技術破壞了邏輯的單調性，傳統(tǒng)的規(guī)范模型已不再適用于捕獲該語言的模型語義。因此，

3、我們提出了極小模型理論并證明了極小模型的存在性定理。 為了正確理解程序語言的執(zhí)行過程，本文研究了MSVL語言的結構化操作語義。首先定義了一種新的適用于描述區(qū)間時序邏輯程序語言語義的表達式格局和命令格局。其次給出了帶有時態(tài)操作符的算術表達式和布爾表達式的求值規(guī)則，以及程序的狀態(tài)遷移系統(tǒng)和區(qū)間遷移系統(tǒng)。狀態(tài)遷移系統(tǒng)包括將一個程序化簡為與其等價的正則形的語義等價規(guī)則和狀態(tài)上的遷移規(guī)則。區(qū)間遷移系統(tǒng)給出了將程序從一個狀態(tài)遷移到下一個狀態(tài)

4、的區(qū)間遷移規(guī)則。進一步，我們研究了兩類遷移系統(tǒng)的性質，并證明了操作語義和基于模型理論的極小模型語義之間的一致性。最后基于本文提出的操作語義，開發(fā)了具有對軟硬件系統(tǒng)進行建模、模擬和驗證功能的MSVL語言的解釋器。 為了實現(xiàn)在同一邏輯框架內對并發(fā)系統(tǒng)進行建模和驗證的目的，本文研究了MSVL語言的公理語義。在該方法中，MSVL語言作為程序設計語言來描述系統(tǒng)行為（系統(tǒng)建模），命題投影時序邏輯作為斷言語言描述系統(tǒng)性質。這樣，系統(tǒng)的模型和性