Deriving protocol specifications from service specifications written as Predicate/Transition-nets

We consider the derivation of a protocol specification from a service specification written in Predicate/Transition-nets (Pr/T-nets). The service specification describes the global behavior of a system and includes the allocation of the Pr/T-net places to N distributed sites. The paper presents a new algorithm for deriving a protocol specification that defines the behavior of N communicating entities that execute on the N sites and coordinate their actions in order to conform to the global behavior defined by the service specification. Our algorithm decomposes each transition of the service specification into a set of communicating Pr/T-subnets running on the N entities. Moreover, for efficiently controlling the conflict for shared resources, we present a timestamp-based contention control algorithm and incorporate it into the derivation algorithm. A tool has been developed that implements our algorithm and works together with other existing tools for the graphical representation of the service and derived protocol specifications. Two application examples are discussed.     

服务组合的代数规约

现有的服务组合描述途径不能有效地验证和测试组合正确性,针对这一问题,提出了一个代数规约方法,引入规约包机制扩展面向服务代数规约语言SOFIA以支持该方法。用代数规约单元描述服务系统中的各种实体,其中基调部分定义实体的语法和结构,公理部分定义其功能和行为特性。与一个服务相关的规约单元封装在一个包中或拆分在几个相互引用的包中,每个包形成一个命名空间。当多个服务组合在一起时,以这些服务的代数规约包为基础,一方面抽象地定义组合服务的交互过程和语义,形成描述服务组合实现方式的实现规约包;另一方面抽象地定义组合服务对外接口及其功能语义,形成描述组合服务需求的抽象规约包。在实现规约和抽象规约的双元结构基础上,进一步定义了实现规约和抽象规约之间必须满足的“实现”关系,证明了满足实现关系可以保证实现的正确性,从而为服务组合的可验证性和可测试性奠定了理论基础。最后结合实例分析阐述了用代数规约描述服务组合的抽象性、可表达性和可验证性。     

Synthesizing Distributed Protocol Specifications from a UML State Machine Modeled Service Specification

The object-oriented paradigm is widely applied in designing and implementing communication systems.Unified Modeling Language(UML) is a standard language used to model the design of object-oriented systems.A protocol state machine is a UML adopted diagram that is widely used in designing communication protocols.It has two key attractive advantages over traditional finite state machines:modeling concurrency and modeling nested hierarchical states.In a distributed communication system,each entity of the system has its own protocol that defines when and how the entity exchanges messages with other communicating entities in the system.The order of the exchanged messages must conform to the overall service specifications of the system.In object-oriented systems,both the service and the protocol specifications are modeled in UML protocol state machines.Protocol specification synthesis methods have to be applied to automatically derive the protocol specification from the service specification.Otherwise,a time-consuming process of design,analysis,and error detection and correction has to be applied iteratively until the design of the protocol becomes error-free and consistent with the service specification.Several synthesis methods are proposed in the literature for models other than UML protocol state machines,and therefore,because of the unique features of the protocol state machines,these methods are inapplicable to services modeled in UML protocol state machines.In this paper,we propose a synthesis method that automatically synthesizes the protocol specification of distributed protocol entities from the service specification,given that both types of specifications are modeled in UML protocol state machines.Our method is based on the latest UML version(UML2.3),and it is proven to synthesize protocol specifications that are syntactically and semantically correct.As an example application,the synthesis method is used to derive the protocol specification of the H.323 standard used in Internet calls.     

On constructing communication protocols from component-based service specifications

Constructing communication protocols from component service specifications, each of which specifies a subfunction of the target protocol, enables efficient development of a large and complex communication protocol. Concerning this construction, related techniques have been already proposed: integration of component protocol specifications into a single protocol specification and transformation of service specifications to protocol specifications. However, the integration needs special knowledge of communication protocols, and the transformation requires that a large and complex service specification should be developed as input to produce the target protocol. In order to cope with these problems, this paper proposes a new method which at first integrates component service specifications into a single service specification, and then transforms the service specification into the target protocol by a protocol synthesis technique. The most important point of view is that component integration is performed at the service specification level rather than the protocol specification level. Additionally, we define a class of ‘well-formed’ service specification which ensures correctness of the target protocol. As a result, the integration and transformation can be efficiently executed in small state space without special knowledge of communication protocols. Finally, we have shown the effectiveness of the proposed method by constructing a part of the real-life OSI protocol FTAM.     

A collision problem in OSI standard formal specifications

A collision problem is presented which can occur between two adjacent protocol entities, a user and its local provider. We consider synchronous and asynchronous communication mechanisms at the Service Access Point between the entities; this is normally an implementation choice. It is shown that even if the problem is limited by using a synchronous communication mechanism, instead of an asynchronous one, it still occurs. We suggest that whenever this case is found, the service provided by the protocol entity must be interpreted differently by its user, ignoring some primitives. When an asynchronous communication mechanism is used, care must be taken to verify that those primitives to be ignored cannot be misinterpreted as new primitives; finally, we point out that the protocol specification could be redesigned to handle these collision cases properly.     

An approach to testing specifications

An approach to testing the consistency of specifications is explored, which is applicable to the design validation of communication protocols and other cases of step-wise refinement. In this approach, a testing module compares a trace of interactions obtained from an execution of the refined specification (e.g., the protocol specification) with the reference specification (e.g., the communication service specification). Nondeterminism in reference specifications presents certain problems. Using an extended finite state transition model for the specifications, a strategy for limiting the amount of nondeterminacy is presented. An automated method for constructing a testing module for a given reference specification is discussed. Experience with the application of this testing approach to the design of a transport protocol and a distributed mutual exclusion algorithm is described.     

Long-lived Rambo: Trading knowledge for communication

Shareable data services providing consistency guarantees, such as atomicity (linearizability), make building distributed systems easier. However, combining linearizability with efficiency in practical algorithms is difficult. A reconfigurable linearizable data service, called Rambo, was developed by Lynch and Shvartsman. This service guarantees consistency under dynamic conditions involving asynchrony, message loss, node crashes, and new node arrivals. The specification of the original algorithm is given at an abstract level aimed at concise presentation and formal reasoning about correctness. The algorithm propagates information by means of gossip messages. If the service is in use for a long time, the size and the number of gossip messages may grow without bound. This paper presents a consistent data service for long-lived objects that improves on Rambo in two ways: it includes an incremental communication protocol and a leave service. The new protocol takes advantage of the local knowledge, and carefully manages the size of messages by removing redundant information, while the leave service allows the nodes to leave the system gracefully. The new algorithm is formally proved correct by forward simulation using levels of abstraction. An experimental implementation of the system was developed for networks-of-workstations. The paper also includes selected analytical and preliminary empirical results that illustrate the advantages of the new algorithm.     

Iterative automatic test generation method for telecommunication protocols

Standardized languages used for protocol specification provide an excellent basis for both automatic and manual test generation. Test generation is composed of two steps, the derivation of test cases from the specification, and the selection of the test cases to be included in the final test suite in order to reduce its execution time. This article proposes a new method that aims to decrease the total number of test cases generated automatically by a test derivation algorithm and at the same time to reduce the computation requirements for the test selection procedure. It creates an iteration cycle on the model of evolutionary algorithms, where the test derivation and selection are done simultaneously. In each cycle first a “small” test suite is derived then optimized, evaluated and finally compared to the best suite so far. It is kept as the best suite, if it is found better according to some well-defined evaluation criteria and test suite metrics. This iteration condition is based on the test selection criteria. The article presents an experiment where iterative algorithms are compared to two simple test derivation methods from different aspects.     

Automatic synthesis of communication controller hardware fromprotocol specifications

Controllers for serial protocols are control-oriented designs that include complex state machines. Manually designing protocol controllers is thus tedious, error prone, and time-consuming. We present a new methodology for the efficient design of communication controller hardware suited for (but not limited to) complex, bit-serial protocols. Our methodology synthesizes controller hardware from a formal high-level specification of the protocol. In this approach, a single run of the synthesis algorithm synthesizes a complete communication architecture from a single protocol specification. The method not only reduces modeling effort but also ensures that both the interacting transaction producer and consumer controllers conform to the initial protocol specification     

基于面向服务架构体系的WEB组合技术应用研究

Web服务是基于XML和HTTPS的一种服务,其通信协议主要基于简单对象访问协议(SOAP),服务的描述通过WSDL、UD-DI来发现和获得服务的元数据。Web服务建好以后,SOAP提供了标准的RPC方法来调用Web service,并意味着下面的Webservice是以对象的方式表示的。SOAP规范定义了SOAP消息的格式,以及怎样通过HTTP协议来使用SOAP。该文基于此,对面向服务架构体系的WEB组合技术应用进行了初步研究。     

Designing secure communication protocols from trust specifications

In a very large distributed system, entities may trust and mistrust others with respect to communication security in arbitrarily complex ways. We formulate the problem of designing a secure communication protocol, given a network interconnection and a ternary relation which captures trust between the entities. We didentify several important ways of synthesizing secure channels, and study the algorithmic problem of designing a secure communication protocol connecting the entities, given the connectivity of the network and the trust relationship between the nodes. We show that whether secure communication is possible can be decided easily in polynomial time. If we also require that channel synthesis proceed along unambiguous paths (in which case the protocol is defined on a spanning tree of the network), we show that the design problem is NP-complete, and we give a linear-time algorithm for an interesting special case of the problem.Research supported by the ESPRIT Basic Research Action No. 3075 ALCOM, a grant from the Volkswagen Foundation to the Universities of Patras and Bonn, and by the NSF.     

Formal models of communication services: a case study

Formal methods can play an important role in exploring new communication systems services. The telecommunications and data communications communities have long accepted the need for formally describing protocols, but only recently have they considered formally describing a service by abstracting specifications from a particular protocol that provides that service. Specifying a service at an abstract level meets two important needs: standardization and customization. The author presents a simplified atomic multicast as an example service and input/output automata for the formal model. He shows how to represent the service specification, a protocol, and implementations of that protocol. He also sketches how to prove the correctness of the protocol and implementation, that is, how to show that the specified service is actually provided     

采用动作时序逻辑的Web服务组合方法

基于有限状态自动机理论,将Web服务建模成一个有限状态自动机。针对网络服务描述语言(WSDL)在服务行为描述方面的缺陷对其进行扩展,提出了从扩展的WSDL到动作时序逻辑(TLA)语言的转换算法,从而可以用TLA对服务行为进行形式化描述和规范,为描述Web服务提供了一个新的方法。讨论了在动作时序逻辑中,服务组合时各组件服务的有限状态自动机的组合方式,以及伴随着服务组合,单个服务的TLA规范如何组合以形成复合服务的TLA规范的问题,并在此基础上,提出了实现TLA规范正确组合的算法思想。     

一种基于ATM的支持并行处理的高速通信机制

随着高速网络（如ＡＴＭ）的发展以及工作站性能的不断提高，工作站网络（ＮＯＷ）作为一种新型的并行计算结构越来越受到人们的重视。传统的传输协议和报文传递系统不能充分作为高速网的传输能力。本文提出一种基于ＡＴＭ的支持并行处理的高速通信机制ＨＰＭＰＡ。在ＨＰＭＰＡ中，可靠的端－端传输协议ＨＳＴＰ为并行应用提供高速可靠的数据传输，而不可靠的端－端传输协议ＵＴＰ则提供不可靠的高速数据报服务，以混合树结构为基础     

Development of an atomic‐broadcast protocol using LOTOS

In this article we report on the development of a group‐communication service using the formal specification language LOTOS, and present our experience in using publicly available tools for this purpose. The service implements atomic broadcast through a Two‐Phase‐Commit protocol, providing at‐least‐once delivery semantics and with no restriction on message delivery order. First we wrote an informal specification describing the desired properties from the service, the interfaces with the underlying network layer and the upper user layer, and the protocol to be used by the service. Then we developed the formal specification of the protocol in LOTOS. After validating the formal specification and thus having a certain confidence in its adequacy with respect to the informal specification, we derived test cases from the formal specification and implemented the service using the Concert/C distributed programming language. While testing the implementation, we found that most errors were related to unspecified features or bugs in the execution environment. From this experience, we draw our conclusions on the usefulness of software development based on formal techniques. Copyright © 1999 John Wiley & Sons, Ltd.     

Process specification generation from communications service specifications

This paper proposes an algorithm for generating process specifications from communications service specifications described by a graph grammar. In this work, it is assumed that a communications system consists of homogeneous processes and that there is no global database. Processes that share a relationship form a global state, and a communications service defines global state transitions caused by inputs to the processes. A global state is represented by a labeled directed graph and a global state transition is described by a graph replacement rule. A process specification is regarded as a distributed algorithm whose purpose is to achieve the global state transitions described by the graph replacement rules. The communication time complexity of the generated distributed algorithm does not depend on the number of graph replacement rules.     

Toward the automation of a QoS-driven SLA establishment in the Cloud

Composite software as a service (SaaS)-based SOA offers opportunities for enterprises to offer value-added services. The cornerstone for such a business is service level agreements between Cloud customers and Cloud providers. In spite of the hype surrounding composite SaaS, standardized methods that enable a reliable management of service level agreements starting from the SLA derivation from the customer requirements to the SLA establishment between the two stockholders are still missing. To overcome such a drawback, we propose a method for SLA establishment guided by QoS for composite SaaS. Our method provides: (1) a requirement specification language for the Cloud customer to define the composition schemas of the requested services along with its QoS constraints; (2) a Cloud provider offer specification language and method to help in identifying the services and resources that satisfy the customer requirements; and (3) an SLA document definition language and method to specify a deployable composite SaaS on the Cloud. Our approach for SLA establishment embraces model-driven architecture principles to automate the SLA document generation from the customer requirements document. The automation is handled through model transformations along with enrichment algorithms to ensure the generation of complete SLA documents.     

CAN总线通信协议的分析和实现

在CAN的技术规范中，只规定了物理层和数据链路层，用户在应用中必须自行定制通信协议，该文以CAN技术规范2.0A为标准，在帧结构的基础上对CAN通信协议的实现作了一定的分析和介绍，为用户设计提供了参考和思路，充分实现CAN的灵活应用。     

基于Axis2的web服务安全框架设计与实现

web服务的广泛应用和网络技术多元化的发展迫切需求一个既能实现web服务安全,又能兼容各种客户端的安全框架.在Axis2的基础上,设计并实现了一个完整的、符合WS-Security规范的web服务框架.框架以文件配置、消息加密和程序控制实现web服务安全,采用SOAP通信协议解决了与各种客户端通信的问题.测试结果表明,此框架可以实现数字签名、消息加密和基于角色的访问控制,能够接收各种基于SOAP协议的客户端请求,具有很好的安全性和兼容性,为企业的web服务安全提供了一个有效的解决方案.