中文摘要：

在对当前面向服务体系架构（service-oriented architecture，简称soA）研究的基础上，给出了一个以企业服务总线（enterpri seservice bus，简称ESB）为中心的面向服务软件体系架构参考模型（SOA reference model，简称SOARM），是集Petri网和时序逻辑于一体的形式化SOA分析、验证和确认方法．基于以客户为中心的面向服务架构设计理念，即根据用户提出系统规范儒求，服务提供者提供服务或组合服务来满足服务消费者，服务接口和ESB作为实现面向服务架构的关键部分虚拟计算环境下，服务语义的一致性验证是十分必要的，SOARM采用新的模式：通过Petri网为服务的行为建模，时序逻辑来描述服务语义一致性约束，综合运用分而治之的精炼检测思想和SOA模型检测合成方法，通过对这些子服务性质的检验来验证整个系统的规范．用商业银行综合前置系统说明了如何使用这种方法来实现面向服务的设计．

英文摘要：

On the basis of the research findings on service-oriented architecture （SOA）, this paper presents a formal systematic SOA analysis, verification and validation methodology called SOARM（SOA reference model） which is the ESB （enterprise service bus）-centric model based on Petri nets and temporal logic. SOARM is consumer-centric, in which the consumers can publish their application specifications/requirements for the service providers to follow when producing or customizing services to support the application. Service interface and enterprise service bus for service realization in service-oriented design are two key parts. When a service is provided or required via the Internet, the semantic consistency becomes the critical issue in the virtualized computing environments. This architecture model tackles the issue by proposing a novel scheme： Petri nets are used to visualize the structure and model the behavior of service architectures while temporal logic is used to specify the required semantic consistency of a service. It is suggested to introduce compositionality in SOA model checking and refinement checking based on the idea of divide-and-conquer, by which the verification task of the whole system is decomposed to several smaller subtasks on the subsystems and shown how to apply it to specify an integrated front-banking system and to analyze its constraints.