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

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

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

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

5、合已有的研究成果,系統(tǒng)的構造基礎抽象狀態(tài)機,復合抽象狀態(tài)機,同步多agent抽象狀態(tài)機和異步多agent抽象狀態(tài)機,從而為系統(tǒng)與軟件提供一個有完善數學背景的設計平臺與方法. (2)受Gurevich的順序抽象狀態(tài)機論題(Sequential ASM Thesis)啟發(fā),初步系統(tǒng)地討論了抽象狀態(tài)機與算法之間的基礎聯系.特別是對于順序算法,綜合已有的理論工作,系統(tǒng)地論證了所有的順序算法都可以被一個適當的順序抽象狀態(tài)機用同樣的步調(st

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

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