面向服务体系结构的连接器规约及其验证

Specifying and verifying Service-Oriented Architectural connectors

连接器建模是软件体系结构设计中研究的重要问题之一。同样,考虑到面向服务体系结构松散耦合的特性,对其所涉及的连接独立于服务的设计进行规约也是一个关键问题。本文将SOA中的服务连接抽象为面向服务设计中的第一类实体--面向服务体系结构的连接器。给出了SOA的连接器模型的规约,并采用π演算作为文中方法的形式化基础以实现对其特性的分析与推理。结合实例给出了SOA连接器的连接语义,并定义了一系列操作原语以规约SOA中与连接器相关的动态重配置和连接器组合。同时,文章用实例展示了文中方法的应用。最后,利用π演算的等价理论及其形式化工具验证了文中方法的正确性。

Architectural connector modeling is one of the most important problems in software architecture design. Similarly, as for Service-Oriented Architecture （SOA）design, a critical issue is to describe its connections in consideration of its loose coupling nature This paper presents an approach to specify service-oriented architectural connectors; at the same time, ＇rr-ealculus is adopted as the formal basis of our approach in order to analyze and reason about the key properties of the model. The connection semantic is given and some operational primitives are defined to capture the dynamic reconfignrations related to connectors as well as connector composition. Finally, we analyze and verify the connector model within an application scenario.