随着软件技术的发展,一种被称为面向服务软件体系结构SOA的软件系统开发方法被提出并得到迅速发展。今天的SOA是基于已经广泛接受的Web服务标准,被誉为下一代Web服务的基础框架。但是目前大多数对SOA的研究仍集中在Web服务标准的拓展、Web服务开发工具以及服务应用集成等方面,对SOA系统架构设计和形式化建模方面的研究还缺乏关注。本文采用一种基于Pi演算的描述语言πADL,对SOA系统的形式化建模过程进行详细的描述和验证。论文首先对面向服务的相关技术和Pi演算基本理论进行阐述。在此基础上给出了服务的相关定义和服务模型,描述了服务的角色、元素、服务属性以及服务之间的交互关系。利用Pi演算对服务、角色以及操作进行定义,以及对服务属性进行详细的描述和分析。本文采用基于移动进程理论Pi演算的描述语言πADL对SOA模型进行形式化规约,为SOA的应用和系统设计提供形式化的描述、分析和验证方法。首先介绍SOA架构的基本结构,包括服务、连接件、系统配置等,然后用πADL直接、显式地对这三部分进行规约。服务是具有统一描述性的组件集合,πADL通过对端口、角色进行规约,从而独立地描述组件、连接件的功能行为。系统配置是服务、连接件按照特定方式组织而成的有机整体,主要研究组件或服务的组装,其中组件组装成服务,服务也可以组装形成组合服务。组装技术包括端口组装、连接件连接以及组装运算操作。论文最后介绍了一个简单SOA系统的建模实例,用专门针对Pi演算开发的自动验证工具移动工作台MWB (Mobility Workbench)来验证SOA模型分析和建模过程的正确性。