A Transport Protocol and Its Formal Description for Local Networks

This paper discusses a transport protocol and its formal description techniques for local network. The transport layer function, the transport services and a transport protocol design in a local network architecture model are presented. A transport protocol specification using the finite state automata (FSA) is given. The correctness of the protocol is verified by using the reachability tree technique with respect to the protocol properties of completeness, deadlock and livelock freeness, termination and reachability.

A Hybrid Formal Description Method Based on FSM,CSP and ADT for Communication Protocol

Since communication protocol deals with complex issues related to distribution such as communication, concurrency and synchronization, their development needs to be traced by using sophisticated formal description methods. This paper presents a new hybrid formal method for communication protocol specification. In this method, finite state machine (FSM), communication sequential process (CSP) and abstract data type (ADT) are mixed and the best features of these approaches are offered. In this paper, the main formal description techniques (FDT) for protocol engineering are brieny introduced and a hybrid formal description method based on the FSM, CSP and ADT for communication protocol is described. Finally, this paper presents the formal specification of an example protocol for LAN by using the proposed hybrid formal method. The results of studies show that the hybrid formal description method for communication protocol is an available and effective approach.

Formalized Description of Distributed Denial of Service Attack

The distributed denial of service (DDoS) attack is one of the dangers in intrusion modes. It's difficult to defense and can cause serious damage to the system. Based on a careful study of the attack principles and characteristics, an object-oriented formalized description is presented, which contains a three-level framework and offers full specifications of all kinds of DDoS modes and their features and the relations between one another. Its greatest merit lies in that it contributes to analyzing, checking and judging DDoS. Now this formalized description has been used in a special IDS and it works very effectively.(

Research on Container Behaviors Protocol

With the development of middleware technology, there are some new features to be adopted on demand in middleware platform based on container component. Aiming at the adaptation of middleware platform, from the nature of component container, this paper begins with behaviors features of EJB （Enterprise Java Bean） container, extracts general behaviors protocol of container, and defines its formal behaviors specification. In the end, the interactive relationship of components is described by WRIGHT language, and the configuration of whole system is shown. The method proposed in this paper mines the hidden features of framework of component container, and applies to refactor middleware platform in reflection and aspect-oriented programming technology.

New Refinement Relations of Z Specifications for Multiple Viewpoints Oriented Requirements Method

In this paper we develop several new refinement relations of Z for multiple viewpoints oriented requirements method (MVORM). The original motivation is that we found the standard Z refinement relation is not adequate or correct when considering specifications that have temporal relationships of operations. The concept of temporal state variables is introduced into Z. Then new implementation relations are defined and new refinement relations are deduced, mainly for temporal state variables to process temporal relationships of operations. We use state transition systems to abstract the temporal state transitions. A simple example is used to show the procedures of MVORM. Finally some directions of further work are forwarded.

Theoretical investigation on the dendritic cells algorithm

The aims of this paper are to helpunderstand the dendritic cells algorithm （DCA） and re- duce the potential incorrect applications and implementations, to clearly present the formal descrip- tion of the dendritic cells algorithm, and to theoretically deduce the algorithm＇ s runtime complexity and detection performance. The entire dendritic cells population of the algorithm is specified using quantitative measures at the functional level. Basic set theory and computational functions, such as addition, multiplication and recursion, are used for clarity and definition, and theoretical analysis is implemented via introduction of three runtime variables in terms of three phases of the algorithm. Consequently, the data structures, procedural operations and pseudocode description of the dendrit- ic cells algorithm are given. The standard DCA achieves a lower bound of ^（n） runtime complexity and an upper bound of O（ n2） runtime complexity under the worst case. In addition, the algorithm＇ s runtime complexity can be improved to O （max（ nN, nS）） by utilizing segmentation approach, where n is the number of input instances, N is the population size and 8 is the size of each segment.