面向服务的企业应用集成系统描述与验证  

Specification and Verification of Service-Oriented Enterprise Application Integration System

作　　者：张广胜[1] 蒋昌俊[1] 汤宪飞[1] 徐岩 

机构地区：[1]同济大学电子与信息工程学院 [2]枣庄农村信用社合作联社,山东枣庄277000

出　　处：《软件学报》2007年第12期3015-3030,共16页Journal of Software

基　　金：Supposed by the National Natural Science Foundation of China under Grant Nos.60534060;60473094(国家自然科学基金);the National High-Tech Research and Development Plan of China under Grant No.2007AA01Z136(国家高技术研究发展计划(863));the National Basic Research Program of China under Grant No.2003CB317002(国家重点基础研究发展计划(973));the 2006 Mountaineering Program ofShanghai;China under Grant No.06JC14065(上海市科委2006年度"登山行动计划")

摘　　要：在对当前面向服务体系架构(service-oriented architecture,简称SOA)研究的基础上,给出了一个以企业服务总线(enterprise service 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.

关 键 词：面向服务的体系架构 体系架构模型 综合前置系统 时序逻辑 PETRI网 形式化描述 正确性验证 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]