分布式计算经过近年来的迅速发展，已形成多种规范或标准，广泛应用于分布式系统设计和开发。然而，这些工业规范或标准明显缺乏坚实的理论基础，从而给分布式系统的规格说明、正确性验证、安全性等工作带来诸多不便。对分布式应用软件系统开发者而言，开发跨平台、跨地域的大型分布式系统仍然是一项相当繁重而复杂的任务。 OMG提出的CORBA(Common Object Request Broker Architecture,CORBA)作为分布式计算标准，仅仅是规范，而不是实现。形式化方法支持大型复杂的软件系统的形式模拟和验证，它可以将软件系统非形式化规范转化为具有严格语义的形式化描述，从而便于系统设计人员阅读、理解、修改、验证和设计开发。因此，从软件系统的形式模拟与验证到实际的开发应用，形式化方法都起着一个重要的桥梁作用。通过对分布式系统的形式化分析，可以查找出系统设计中的漏洞或缺陷，能够帮助设计者修改和优化系统，使其更规范、有效、合理。 形式化方法对分布式计算理论模型研究主要是将涉及分布与并发行为的各种概念形式化，从而给出这些行为的精确定义，避免系统开发人员理解上的二义性，并且为系统开发人员提供可靠的数学工具，用于说明、设计和验证分布式系统的多个方面，如系统运行的正确性、安全性等。显然，开发分布式系统比传统的集中式系统更需要一种精确的数学模型。 目前，国内外可用于分布式系统形式描述与验证的形式化方法主要分为四大类：基于模型的方法、基于逻辑方法、基于进程演算的方法，以及基于网络的方法等等。本文在综合分析并比较了它们的应用特点及不足后，以Petri网为形式化工具，研究了基于CORBA分布式系统的建模技术。本文研究工作的主要贡献表现在如下几个方面： (1) 从理论上研究并分析了CORBA对象服务规范与其扩展着色Petri网模型的动态行为一致性。分析表明扩展着色Petri网模型不仅能够清楚描述系统对象的静态行为，同时也能极好地模拟系统分布性和动态性。 (2) 对于分布式系统的安全性，本文应用标注着色Petri网模拟技术，明确描述和分析了CORBA分布式系统主体责任、证据等与安全性有关的重要性质，并研究了分布式系统不可否认性的模拟验证技术。 (3) 用时序Petri网模拟和分析了分布式系统的ACID事务处理，为构建基于CORBA的事务处理系统提供了分析方法。此外，本文综合应用时间Petri网和工作流网的概念，研究并分析了分布式系统工作流的形式化模拟技术和验证方法。