基于抽象狀態(tài)機(jī)的計算模型及應(yīng)用研究.pdf

1、抽象狀態(tài)機(jī)(Abstract State Machines,ASM)的基本思想可以追溯到上個世紀(jì)80年代.ASM的發(fā)明者Yuri Gurevich從數(shù)學(xué)領(lǐng)域轉(zhuǎn)到計算機(jī)領(lǐng)域發(fā)現(xiàn)這樣的現(xiàn)象:一個程序語言在不同的編譯器下有著不同的編譯.這就存在一個問題:究竟一個程序語言的確切語義是什么? 為了上面的問題,Yuri Gurevich進(jìn)行研究的初衷是:(1)為Church.Turing論題引入資源邊界的限制;(2)采用動態(tài)結(jié)構(gòu)(Dynami

2、c structures)定義更為抽象的計算設(shè)備.Yuri Gurevich從數(shù)學(xué)中得到了啟迪,任何靜態(tài)的數(shù)學(xué)實體,都可以表示為一階結(jié)構(gòu),因而算法的每個狀態(tài)為一階結(jié)構(gòu).計算(Computation)就是狀態(tài)的進(jìn)化(Evolving).可以容易的用一個函數(shù)來表示一個關(guān)系,使得一階結(jié)構(gòu)中可以只含有函數(shù),而只有函數(shù)運算的結(jié)構(gòu)在泛代數(shù)(Universal Algebras)中稱為代數(shù).因此這種模型最初被分別稱為動態(tài)結(jié)構(gòu)(Dynamic Stru

3、ctures),動態(tài)代數(shù)(Dynamic Algebras),以及進(jìn)化代數(shù)(=Evolving Algebras).最終,通過多年的研究,人們發(fā)現(xiàn)進(jìn)化代數(shù)實際上是Dj.jl(stra的抽象機(jī)(Abstract Machine)的基本概念和利用Tarski的結(jié)構(gòu)作為一般的抽象狀態(tài)(Abstract States)的基本思想的完美結(jié)合,最終稱為抽象狀態(tài)機(jī).所以ASM=Abstract State+Abstract Machine. 目

4、前,ASM已經(jīng)從一種思想發(fā)展成一種成熟的模型,一種語言,一種被國際標(biāo)準(zhǔn)化組織承認(rèn)的、在軟件和硬件規(guī)約中廣泛使用的工具.同時ASM的工業(yè)用軟件開發(fā)環(huán)境已經(jīng)初露端倪,并且已經(jīng)得到成功的運用.值得一提的是,在Microsoft的大力支持和推動下,已經(jīng)產(chǎn)生了ASM Language(即AsmL并整合到了.Net開發(fā)環(huán)境中. 本文選擇抽象狀態(tài)機(jī)作為研究目標(biāo),探討其理論基礎(chǔ)與應(yīng)用環(huán)境,主要內(nèi)容有如下幾個方面: (1)從其數(shù)學(xué)基礎(chǔ)出發(fā),綜

5、合已有的研究成果,系統(tǒng)的構(gòu)造基礎(chǔ)抽象狀態(tài)機(jī),復(fù)合抽象狀態(tài)機(jī),同步多agent抽象狀態(tài)機(jī)和異步多agent抽象狀態(tài)機(jī),從而為系統(tǒng)與軟件提供一個有完善數(shù)學(xué)背景的設(shè)計平臺與方法. (2)受Gurevich的順序抽象狀態(tài)機(jī)論題(Sequential ASM Thesis)啟發(fā),初步系統(tǒng)地討論了抽象狀態(tài)機(jī)與算法之間的基礎(chǔ)聯(lián)系.特別是對于順序算法,綜合已有的理論工作,系統(tǒng)地論證了所有的順序算法都可以被一個適當(dāng)?shù)捻樞虺橄鬆顟B(tài)機(jī)用同樣的步調(diào)(st

6、ep for step)模擬.同時針對非確定性算法也作了相關(guān)的探討. (3)為Web服務(wù)中的Business Process Execution Language for Web Set-vices(BPEL)定義了一個分布式抽象狀態(tài)機(jī)(DASM),基于抽象狀態(tài)機(jī)的理論背景,BPEL有更清晰和完備的數(shù)學(xué)意義.整個模型的執(zhí)行是由協(xié)作與反應(yīng)行為來刻畫,具備擴(kuò)充復(fù)雜業(yè)務(wù)過程的能力. (4)通過建立抽象狀態(tài)機(jī)與關(guān)系轉(zhuǎn)換器之間的聯(lián)系,

7、詳細(xì)探討了電子商務(wù)中的若干驗證問題,并給出了問題的形式化方式.相對于其他的關(guān)系轉(zhuǎn)換器,ASM關(guān)系轉(zhuǎn)換器具備更強(qiáng)的計算能力.并且利用已有的邏輯與模型驗證的結(jié)論,說明了驗證問題的復(fù)雜性范圍,以及為了限制驗證問題的復(fù)雜性所需要做的約束. (5)基于抽象狀態(tài)機(jī)來刻畫移動對象的語義.基于抽象狀態(tài)機(jī)建立的移動系統(tǒng)依賴于語義規(guī)范單元的交互抽象,移動性通過通訊拓?fù)浣Y(jié)構(gòu)的動態(tài)變化來表示.并且參考進(jìn)程代數(shù)的形式系統(tǒng),同樣強(qiáng)調(diào)通訊的通道可以通過其它通道