抽象状态机(Abstract State Machines,ASM)的基本思想可以追溯到上个世纪80年代.ASM的发明者Yuri Gurevich从数学领域转到计算机领域发现这样的现象:一个程序语言在不同的编译器下有着不同的编译.这就存在一个问题:究竟一个程序语言的确切语义是什么? 为了上面的问题,Yuri Gurevich进行研究的初衷是:(1)为Church.Turing论题引入资源边界的限制;(2)采用动态结构(Dynamic structures)定义更为抽象的计算设备.Yuri Gurevich从数学中得到了启迪,任何静态的数学实体,都可以表示为一阶结构,因而算法的每个状态为一阶结构.计算(Computation)就是状态的进化(Evolving).可以容易的用一个函数来表示一个关系,使得一阶结构中可以只含有函数,而只有函数运算的结构在泛代数(Universal Algebras)中称为代数.因此这种模型最初被分别称为动态结构(Dynamic Structures),动态代数(Dynamic Algebras),以及进化代数(=Evolving Algebras).最终,通过多年的研究,人们发现进化代数实际上是Dj.jl(stra的抽象机(Abstract Machine)的基本概念和利用Tarski的结构作为一般的抽象状态(Abstract States)的基本思想的完美结合,最终称为抽象状态机.所以ASM=Abstract State+Abstract Machine. 目前,ASM已经从一种思想发展成一种成熟的模型,一种语言,一种被国际标准化组织承认的、在软件和硬件规约中广泛使用的工具.同时ASM的工业用软件开发环境已经初露端倪,并且已经得到成功的运用.值得一提的是,在Microsoft的大力支持和推动下,已经产生了ASM Language(即AsmL并整合到了.Net开发环境中. 本文选择抽象状态机作为研究目标,探讨其理论基础与应用环境,主要内容有如下几个方面: (1)从其数学基础出发,综合已有的研究成果,系统的构造基础抽象状态机,复合抽象状态机,同步多agent抽象状态机和异步多agent抽象状态机,从而为系统与软件提供一个有完善数学背景的设计平台与方法. (2)受Gurevich的顺序抽象状态机论题(Sequential ASM Thesis)启发,初步系统地讨论了抽象状态机与算法之间的基础联系.特别是对于顺序算法,综合已有的理论工作,系统地论证了所有的顺序算法都可以被一个适当的顺序抽象状态机用同样的步调(step for step)模拟.同时针对非确定性算法也作了相关的探讨. (3)为Web服务中的Business Process Execution Language for Web Set-vices(BPEL)定义了一个分布式抽象状态机(DASM),基于抽象状态机的理论背景,BPEL有更清晰和完备的数学意义.整个模型的执行是由协作与反应行为来刻画,具备扩充复杂业务过程的能力. (4)通过建立抽象状态机与关系转换器之间的联系,详细探讨了电子商务中的若干验证问题,并给出了问题的形式化方式.相对于其他的关系转换器,ASM关系转换器具备更强的计算能力.并且利用已有的逻辑与模型验证的结论,说明了验证问题的复杂性范围,以及为了限制验证问题的复杂性所需要做的约束. (5)基于抽象状态机来刻画移动对象的语义.基于抽象状态机建立的移动系统依赖于语义规范单元的交互抽象,移动性通过通讯拓扑结构的动态变化来表示.并且参考进程代数的形式系统,同样强调通讯的通道可以通过其它通道传输,从而进程可以动态地获取新通道.相比较于进程代数,基于抽象状态机的移动系统在软件工程方面易于实现和扩展.