随着计算机技术和网络技术的发展，移动计算与实时计算已经成为计算机科学领域的两个研究热点，受到越来越多的关注。不同领域的学者对这一问题的研究有不同的方法。形式化方法作为研究分布式、并发计算的一个重要重要方法，近年来得到了飞速的发展。形式化专家们提出了许多移动计算和实时计算的形式系统：如自动机、petri网、CCS、Pi演算、Mobile Ambients等。这些形式系统可以刻画、研究并发分布式系统，传值计算以及空间移动系统。但是它们各有特色，比方说Pi演算适合于传值计算；而Mobile Ambients在空间移动计算系统中更能够发挥自己的优势。实时计算作为近年计算机科学领域的另一个研究的热点，形式化专家也提出了它的形式化框架。这些实时形式化框架主要是用时间对原有的形式系统的扩展。新的形式化框架能够研究计算机系统在时间方面的性质，已有的实时系统有Timed Automata，Timed CCS，实时Pi演算等，但这些实时形式系统由于扩展前原型系统的局限性，不能表示空间结构。通过以Mobile Ambients演算为基础的实时扩充，可以很好的将时空统一到同一个形式化框架中研究。本文首先讨论了Mobile Ambients的优点和不足，然后提出一种基于图的实时移动计算模型，接下来用时间对Mobile Ambients进行扩展，提出了一种新的实时形式化系统——离散实时Mobile Ambients。对一个系统作模型验证，不仅需要将系统用形式语言表示，而且还要将系统要求满足的性质表示成模态逻辑公式。为利用离散实时Mobile Ambients对实时移动计算系统做模型验证，本文对Mobile Ambients的时态逻辑也作了扩展，提出了能够描述实时性质的模态逻辑。最后对离散实时Mobile Ambients演算的子集提出了模型验证算法，并且用离散实时Mobile Ambients演算建模Web服务组合语言BPEL4WS。本文的主要内容包括以下几个部分：第一，讨论了mobile ambients的优缺点，并且提出了基于图的实时移动计算模型；第二，对Mobile Ambients作实时扩展，提出新的实时形式系统——离散实时Mobile Ambients；第三，提出离散实时Mobile Ambients演算的时态逻辑，给出离散实时Mobile Ambients的模型验证算法，并给出离散实时Mobile Ambients演算模型验证的可判定性的证明。第四，利用离散实时Mobile Ambients建模Web服务组合语言BPEL4WS，对一个Web服务实例进行模型验证。最后，总结全文工作，并展望了以后的前景。