Worms are a common phenomenon in today's Internet and cause tens of billions of dollars in damages to businesses around the world each year. This article first presents various concepts related to worms, and then classifies the existing worms into four types- Internet worms, P2P worms, email worms and IM (Instant Messaging) worms, based on the space in which a worm finds a victim target. The Internet worm is the focus of this article. We identify the characteristics of Internet worms in terms of their target finding strategy, propagation method and anti-detection capability. Then, we explore state-of-the-art worm detection and worm containment schemes. This article also briefly presents the characteristics, defense methods and related research work of P2P worms, email worms and IM worms. Nowadays, defense against worms remains largely an open problem. In the end of this article, we outline some future directions on the worm research.

A desired property of large distributed systems is self adaptability against the faults that occur more frequently as the size of the distributed system grows. Self-stabilizing protocols provide autonomous recovery from finite number of transient faults. Fault-containing self-stabilizing protocols promise not only self-stabilization but also containment of faults (quick recovery and small effect) against small number of faults. However, existing composition techniques for self-stabilizing protocols (e.g. fair composition) cannot preserve the fault-containment property when composing fault-containing self-stabilizing protocols. In this paper, we present Recovery Waiting Fault-containing Composition (RWFC) framework that provides a composition of multiple fault-containing self-stabilizing protocols while preserving the fault-containment property of the source protocols.

There are two approaches for formal verification of sequential designs or finite state machines: language containment checking and symbolic model checking. To verify designs of practical size, in these two approaches, designs are represented symbolically, in practice, by ordered binary decision diagrams. In the conventional algorithm for language containment checking, finite automata given as specifications are also represented symbolically. This paper proposes a new method, called partially explicit method for checking language containment. By representing states of finite automata given as specifications explicitly, this method can remove redundant computations, and as a result, provide better performance than the conventional method which uses the product machines of designs and specifications. The experimental results show that this approach is effective in checking language containment symbolically.

A pattern is a finite string of constant symbols and variable symbols. The language of a pattern is the set of all strings obtained by substituting any nonnull constant string for each variable symbol in the pattern. The class of pattern languages was introduced by Angluin in 1979 as a concrete class which is inferable from positive data. In this paper, we consider the decision problem whether for given two patterns there is a containment relation between their languages, which was posed by Angluin and its decidability remains open. We give some sufficient conditions to make this problem decidable. We also introduce the notions of generalizations and minimal generalizations common to a set of patterns. We characterize the above open problem using the minimal generalization.