近年来，随着计算机科学技术，特别是Internet技术的飞速发展，软件运行的平台正由传统的静态封闭走向现在的动态开放，软件的计算模式也由已往的单个个体之间的串行进行发展到今天多个实体之间进行交互和合作。如何在这样一个动态开放的环境下，实现软件实体之间通过网络，特别是Internet进行共享和合作成了今天软件技术所面临的一个重大的挑战，而软件协同技术业已成为解决这一问题的一个重要途径。软件协同作为一种新型的软件范型，由软件实体和它们之间的交互构成；软件实体与其交互的分离很好地体现了软件工程中关注分离的原则，使得应用系统的可追溯性和可复用性更强，并可支持全局分析。 目前对软件协同的研究主要集中在协同语言，协同模型和协同系统之上。协同模型和语言主要用于在应用的合作模型和底层的通信模型之间架设一个桥梁作用。协同模型在高层描述软件实体应如何进行交互；而协同语言是协同模型的语言级的对应。基于协同模型和语言，可以建立实际可行的协同系统。注意到软件协同往往牵涉到多个软件实体之间的并发交互，正是因为此，目前的应用系统往往显得较为复杂，容易引发错误，从而难以进行高效的开发和维护，同时它们必须满足严格的正确性、可靠性和安全性需求。形式化方法是一种以数学理论作为坚实的基础，能够提供系统且全面的对计算机系统进行描述、分析和验证的方法，从而被广泛认为是一种行之有效的减少设计错误、提供系统可靠性的方法。本文从形式化方法的角度来研究软件协同。 验证系统的正确性是采用形式化方法的一个主要目的。系统验证包含系统建模和系统规约过程。系统建模可以被认为是系统验证的第一步，模型描述了系统如何运作。它一方面要保留和性质相关的部分，另一方面要抽象掉那些复杂的且与所验证性质无关的部分。针对软件协同，设计合适的演算是一种被广泛认可的有广阔前景的对软件协同系统进行建模的方法。一般而言，演算可以被看成是一种小型的程序设计语言，它能够提供对计算的简洁描述，并可以基于此进行严格的分析。系统规约描述了系统应该如何进行，通常采用模态逻辑或者时序逻辑来书写系统规约，它们可以描述那些随时间变化系统的性质。 在系统建模方面，本文主要采用进程代数作为系统模型。进程代数是以代数的手段和方法来研究系统进程的行为，包括一个系统可以执行的事件或者动作。进程代数是系统建模的一个重要的方法，它们提供一个可以精确描述计算的手段以利于进行严格的分析。一般而言，进程演算具有一个精确的语法和一个可计算的操作语义。在我们的工作中，主要研究了π演算和移动环境演算这两种具有代表性的进程演算及其变例。事实上，π演算是一种可以描述系统拓扑结构随时间变化的演算。系统拓扑结构的改变体现在link之间的移动。π演算通过忽视变量，通信信道，常数和普通数据之间的差异，统一以名的形式表示出来，并把计算表示为名之间通过link进行通信。而移动环境演算能够显式地描述进程的位置和移动原语。移动环境演算可以描述动态改变其位置并在移动前后保持活跃性的计算。 在系统规约方面，本文主要采用空间逻辑和树逻辑作为系统规约手段，这两种逻辑可以描述位置，处所以及空间的性质。一般而言，空间逻辑由四部分操作子构成，分别为标准命题逻辑连接子，空间操作子，时序模态子和面向演算的操作子。针对不同的应用，我们可以裁剪标准空间逻辑，即加入或减少一些算子以适合不同的应用需求，比如与环境演算相关的算子或者不动点构造等等。在本文的工作中，我们主要选取空间逻辑中的静态部分，即不包含时序模态子。 在验证方法上，我们主要采用基于逻辑的模型检测作为主要手段。基于逻辑的模型检测是给定一个模型和一个逻辑公式，它能够确定模型的哪些状态符合这个逻辑公式。模型检测的一个最大的优点在于它的全自动性。模型检测的结果有三种可能，如果是肯定的结果，那说明该模型满足该公式；如果是否定的结果，我们将得到一个反例来说明为什么该模型不满足该公式；另一种可能性是状态空间爆炸使得内存不足而没有结果，这是模型检测方法的一个缺点，目前有很多研究工作是致力于减少或压缩状态空间，比如状态的符号化表示，on-the—fly的算法，