There are two ways to describe a state machine as an algebraic specification: a behavioral specification and a rewrite specification. In this study, we propose a translation system from behavioral specifications to rewrite specifications to obtain a verification system which has the strong points of verification techniques for both specifications. Since our translation system is complete with respect to invariant properties, it helps us to obtain a counter-example for an invariant property through automatic exhaustive searching for a rewrite specification.

The Bloom Filter (BF), a space-and-time-efficient hash-coding method, is used as one of the fundamental modules in several network processing algorithms and applications such as route lookups, cache hits, packet classification, per-flow state management or network monitoring. BF is a simple space-efficient randomized data structure used to represent a data set in order to support membership queries. However, BF generates false positives, and cannot count the number of distinct elements. A counting Bloom Filter (CBF) can count the number of distinct elements, but CBF needs more space than BF. We propose an alternative data structure of CBF, and we called this structure an Adaptive Bloom Filter (ABF). Although ABF uses the same-sized bit-vector used in BF, the number of hash functions employed by ABF is dynamically changed to record the number of appearances of a each key element. Considering the hash collisions, the multiplicity of a each key element on ABF can be estimated from the number of hash functions used to decode the membership of the each key element. Although ABF can realize the same functionality as CBF, ABF requires the same memory size as BF. We describe the construction of ABF and IABF (Improved ABF), and provide a mathematical analysis and simulation using Zipf's distribution. Finally, we show that ABF can be used for an unpredictable data set such as real network traffic.

This paper considers the problem of contention resolution algorithm for multi-class with quality of service (QoS) constrained for wireless communication. Five different channel reservation schemes are proposed, namely, UNI+MLA, UNI+DS, UNI+DS+MLA, Partial UNI and Partial UNI+MLA schemes for multimedia traffic, all are extensions of our recently proposed UNI scheme for single-class traffic. The goal is to achieve the highest system performance and enable each traffic type to meet its QoS requirements. We evaluate the performance of each scheme by mathematical analysis. The numerical results show that our proposed schemes are effective in enabling each traffic type to achieve the best successful rate possible in this kind of environment. Finally when comparing between our proposed schemes and conventional technique in terms of both throughput performance and QoS requirements it is found that the UNI+MLA, UNI+DS+MLA and Partial UNI+MLA schemes are relatively efficient and suitable for practical applications.

This paper proposes two traffic control schemes to support the communication quality of multimedia streaming services such as VoIP and audio/video over IEEE 802.11 wireless LAN systems. The main features of the proposed scheme are bandwidth control for each flow of the multimedia streaming service and load balancing between access points (APs) of the wireless LAN by using information of data link, network and transport layers. The proposed schemes are implemented on a Linux machine which is called the wireless traffic controller (WTC). The WTC connects a high capacity backbone network and an access network to which the APs are attached. We evaluated the performance of the proposed WTC and confirmed that the communication quality of the multimedia streaming would be greatly improved by using this technique.

IEEE 802.11 wirelesses LANs (WLANs) have been rapidly deployed in enterprises, public areas, and households. Voice-over-IP (VoIP) and similar applications are now commonly used in mobile devices over wireless networks. Recent works have improved the quality of service (QoS) offering higher data rates to support various kinds of real-time applications. However, besides the need for higher data rates, seamless handoff and load balancing among APs are key issues that must be addressed in order to continue supporting real-time services across wireless LANs and providing fair services to all users. In this paper, we introduce a novel access point (AP) with two transceivers that improves network efficiency by supporting seamless handoff and traffic load balancing in a wireless network. In our proposed scheme, the novel AP uses the second transceiver to scan and find neighboring STAs in the transmission range and then sends the results to neighboring APs, which compare and analyze whether or not the STA should perform a handoff. The initial results from our simulations show that the novel AP module is more effective than the conventional scheme and a related work in terms of providing a handoff process with low latency and sharing traffic load with neighbor APs.

We describe a sub 100-mW H.264 MP@L4.1 integer-pel motion estimation processor core for low power video encoder. It supports macro block adaptive frame field (MBAFF) encoding and bi-directional prediction for a resolution of 19201080 pixels at 30 fps. The proposed processor features a novel hierarchical algorithm, reconfigurable ring-connected systolic array architecture and segmentation-free, rectangle-access search window buffer. The hierarchical algorithm consists of a fine search and a coarse search. A complementary recursive cross search is newly introduced in the coarse search. The fine search is adaptively carried out, based on an image analysis result obtained by the coarse search. The proposed systolic array architecture minimizes the amount of transferred data, and lowers computation cycles for the coarse and fine searches. In addition, we propose a novel search window buffer SRAM that has instantaneous accessibility to a rectangular area with arbitrary location. The processor core has been designed with a 90 nm CMOS design rule. Core size is 2.52.5 mm2. One core supports one-reference-frame and dissipates 48 mW at 1 V. Two core configuration consumes 96 mW for two-reference-frame search.

We present a new framework for checking safety failures. The approach is based on the conservative inference of the internal states of a system by the observation of the interaction with its environment. It is based on two similar mechanisms : forward implication, which performs the analysis of the consequences of an input applied to the system, and backward implication, that performs the same task for an output transition. While being a very simple approach, it is general and we believe it can yield efficient algorithms in different safety-failure checking problems. As a case study, we have applied this framework to an existing problem, the hazard checking in (speed-independent) asynchronous circuits. Our new methodology yields an efficient algorithm that performs better or as well as all existing algorithms, while being more general than the fastest one.

In order to achieve the prioritized quality of service (QoS) guarantee, the IEEE 802.11e EDCAF (the enhanced distributed channel access function) provides the distinguished services by configuring the different QoS parameters to different access categories (ACs). An admission control scheme is needed to maximize the utilization of wireless channel. Most of papers study throughput improvement by solving the complicated multidimensional Markov-chain model. In this paper, we introduce a backoff model to study the transmission probability of the different arbitration interframe space number (AIFSN) and the minimum contention window size (CWmin). We propose an adaptive control scheme (ACS) to dynamically update AIFSN and CWmin based on the periodical monitoring of current channel status and QoS requirements to achieve the specific service differentiation at access points (AP). This paper provides an effective tuning mechanism for improving QoS in WLAN. Analytical and simulation results show that the proposed scheme outperforms the basic EDCAF in terms of throughput and service differentiation especially at high collision rate.

A new load balanced channel sharing method (CSM), namely Heuristic Traffic Load Balanced (HTLB) CSM, is proposed for metro-wavelength division multiple access (WDMA) networks. In particular, HTLB CSM is designed to be effective for pre-allocation based medium access control (MAC) protocols by balancing traffic loads corresponding to pre-assigned destinations per time slot. As a result, HTLB CSM is shown to provide lower time complexity than the well-known sub-optimal load balanced CSM, MULTIFIT CSM. Furthermore, the Jain Index of the HTLB CSM is shown to be higher and more consistent than the MULTIFIT CSM and other pre-fixed CSMs under diverse traffic conditions.

In this paper, we consider a method to enhance the throughput of HSDPA systems in the mixed traffic scenario. A channel-dependent adaptive delay barrier (DB) function is proposed to maximize throughput of best-effort (BE) traffic while satisfying the delay latency of voice over internet protocol (VoIP) service. Simulations show that the proposed channel-adaptive DB function raises the throughput of BE traffic service by 30% compared to the conventional scheme, without degrading the capacity of VoIP service over HSDPA system.

Recently problems with commercial IP telephony systems have been reported one after another, in Japan. One of the important causes is congestion in the control plane. It has been recognized that with the current Internet it is important to control not only congestion caused by overload of the data plane but also congestion caused by overload of the control plane. In particular, "retry traffic," such as repeated attempts to set up a connection, tends to cause congestion. In general, users make repeated attempt to set up connections not only when the data plane is congested but also when the control plane in the network is overloaded. The latter is caused by user behavior: an increase in the waiting time for the processing of connection establishment to be completed tends to increase his or her initiation of reattempts. Thus, it is important to manage both data plane and control-plane resources effectively. In this paper, we focus on RSVP-based communication services including IP telephony, and introduce a model that takes account of both data-plane and control-plane systems, and we examine the behavior of retry traffic. In addition, we compare the system stability achieved by two different resource management methods, the hard-state method and the soft-state method.

The call-level performance modelling is a challenge in the highly heterogeneous environment of modern telecom networks, due to the presence of elastic traffic. In this paper, we review existing teletraffic loss models and propose a model for elastic traffic of service-classes with finite population (quasi-random call arrival process). Upon arrival, calls have contingency alternative bandwidth requirements that depend on thresholds which indicate the available/occupied link bandwidth (state dependent model). Calls are admitted under the complete sharing policy, and can tolerate bandwidth compression, while in-service. We prove a recurrent formula for the efficient calculation of the link occupancy distribution and consequently the call blocking probabilities and link utilization. The accuracy of the proposed model is verified by simulation and is found to be quite satisfactory. Comparative results with other existing models show the necessity and the effectiveness of the proposed model. Its potential applications are mainly in the environment of wireless networks.

This letter proposes a novel method of large-scale IP traffic matrix estimation which is based on Partial Flow Measurement and Fratar Model (PFMFM). Firstly, we model OD flows as Fratar model and introduce the constrained relations between traffic matrix and link loads. By combining partial flow measurement, we can get a good prior value of network tomography. Then a good estimation of traffic matrix is attained with the modified network tomography method. Finally, we use the real data [8] from network Abilene to validate our method. In contrast to TomoGravity [1], the results show that our method improves remarkably and the estimation of traffic matrix is closer to real data, and especially when the flow is small and changes dramatically, the estimation is better.

The time division duplex cellular system can support various downlink and uplink traffic ratios by setting the downlink and uplink transmission periods appropriately. However, it causes severe co-channel interference problem when some cells are active in the downlink while the others are in the uplink [2]. To mitigate this problem, a resource allocation scheme combined with sectorization is proposed for orthogonal frequency division multiple access. Simulations demonstrate that the proposed scheme improves both spectral efficiency and outage performance compared to the conventional allocation schemes.

The clonal selection algorithm (CS), inspired by the basic features of adaptive immune response to antigenic stimulus, can exploit and explore the solution space parallelly and effectively. However, antibody initialization and premature convergence are two problems of CS. To overcome these two problems, we propose a chaotic distance-based clonal selection algorithm (CDCS). In this novel algorithm, we introduce a chaotic initialization mechanism and a distance-based somatic hypermutation to improve the performance of CS. The proposed algorithm is also verified for numerous benchmark traveling salesman problems. Experimental results show that the improved algorithm proposed in this paper provides better performance when compared to other metaheuristics.

In this study, we propose a simple, yet general and powerful framework for constructing accurate affine invariant regions. In our framework, a method for extracting reliable seed points is first proposed. Then, regions which are invariant to most common affine transformations can be extracted from seed points by two new methods the Path Growing (PG) or the Thresholding Seeded Growing Region (TSGR). After that, an improved ellipse fitting method based on the Direct Least Square Fitting (DLSF) is used to fit the irregularly-shaped contours from the PG or the TSGR to obtain ellipse regions as the final invariant regions. In the experiments, our framework is first evaluated by the criterions of Mikolajczyk's evaluation framework [1], and then by near-duplicate detection problem [2]. Our framework shows its superiorities to the other detectors for different transformed images under Mikolajczyk's evaluation framework and the one with TSGR also gives satisfying results in the application to near-duplicate detection problem.

We explain how network failures were caused by a natural disaster, describe the restoration steps that were taken, and present lessons learned from the recovery. At 21:26 on December 26th (UTC+9), 2006, there was a serious undersea earthquake off the coast of Taiwan, which measured 7.1 on the Richter scale. This earthquake caused significant damage to submarine cable systems. The resulting fiber cable failures shut down communications in several countries in the Asia Pacific networks. In the first post-earthquake recovery step, BGP routers detoured traffic along redundant backup paths, which provided poor quality connection. Subsequently, operators engineered traffic to improve the quality of recovered communication. To avoid filling narrow-bandwidth links with detoured traffic, the operators had to change the BGP routing policy. Despite the routing-level first aid, a few institutions could not be directly connected to the R&E network community because they had only a single link to the network. For these single-link networks, the commodity link was temporarily used for connectivity. Then, cable connection configurations at the switches were changed to provide high bandwidth and next-generation Internet service. From the whole restoration procedure, we learned that redundant BGP routing information is useful for recovering connectivity but not for providing available bandwidth for the re-routed traffic load and that collaboration between operators is valuable in solving traffic engineering issues such as poor-quality re-routing and lost connections of single-link networks.

This paper tries to answer the following question: What type of support should be given to an automobile driver when it is determined, via some method to monitor the driver's behavior and the traffic environment, that the driver's intent may not be appropriate to a traffic condition? With a medium fidelity, moving-base driving simulator, three conditions were compared: (a) Warning type support in which an auditory warning is given to the driver to enhance his/her situation recognition, (b) action type support in which an autonomous safety control action is executed to avoid an accident, and (c) the baseline condition in which no driver support is given. Results were as follows: (1) Either type of driver support was effective in accident prevention. (2) Acceptance of driver support functions varied context dependently. (3) Participants accepted a system-initiated automation invocation as long as no automation surprises were possible to occur.

This paper proposes a notion of a controllability measure of discrete-time piecewise affine systems, which is a natural extension of the controllability gramian of linear systems. Although this measure is calculated in a probabilistic way, it may be applied to control of biological systems for providing a policy to experiments for pharmaceutical developments. Thus an application to gene regulatory control of luminescence in the marine bacterium modeled by the piecewise affine system is discussed in this paper.

We propose a packet sampling strategy called fixed-period sampling, which selects at most one packet in every fixed-length period. Under the fixed-period sampling, the number of flow-cache lookups during a unit of time or the number of entries in a flow cache is bounded by a constant, which is simply expressed by a few tuning parameters. As an application of the fixed-period sampling, we also focus on the flow-rate estimation from fixed-period sampled packet streams. In particular, we propose a simple estimator based solely on the sampling frequency. We have conducted simulation experiments using two real traces to show basic characteristics of the fixed-period sampling for the comparison with the fixed-period sampling. We also show the accuracy of the proposed flow-rate estimator through simulations.