State Transition Matrix (STM) is a table-based modeling language that has been frequently used in industry for specifying behaviors of systems. Functional correctness of a STM design (i.e., a design developed with STM) could often be expressed as invariant properties. In this paper, we first present a formalization of the static and dynamic aspects of STM designs. Consequentially, based on this formalization, we investigate a symbolic encoding approach, through which a STM design could be bounded model checked w.r.t. invariant properties by using Satisfiability Modulo Theories (SMT) solving technique. We have built a prototype implementation of the proposed encoding and the state-of-the-art SMT solver - Yices, is used in our experiments to evaluate the effectiveness of our approach. Two attempts for accelerating SMT solving are also reported.

We study behavior of multi-zone MCA (Multi-Channel Access) mobile communication systems with a finite number of channels in each zone. Three queueing schemes for channel requests named holding scheme, ready-nonready scheme, and optimum scheme are investigated. The delay performance of channel requests is studied through computer simulations.

With the advance of computer technologies, mobile computers can hold many local resources in themselves. In many cases it is impossible to announce local resources on them because almost information announcement systems are not designed for them. In this paper, an information announcement system for mobile computers based on WWW is proposed. The system efficiently announces resources on mobile computers independently of whether they are connected to a network or not, and wherever they are connected. The system can also select suitable announcement methods according to the type of resources. We implement a prototype of proposed system and evaluate it. The result of evaluation confirms effectiveness of the proposed system.

Data caching is widely known as an effective power-saving technique, in which mobile devices use local caches instead of original data placed on a server, in order to reduce the power consumption necessary for network accesses. In such data caching, a cache invalidation mechanism is important in preventing these devices from unintentionally accessing invalid data. In this paper, we propose a broadcast-based protocol for cache invalidation in a location-aware system. The proposed protocol is designed to reduce the access time required for obtaining necessary invalidation reports through broadcast media and to avoid client-side sleep fragmentation while retrieving the reports. In the proposed protocol, a Bloom filter is used as the data structure of an invalidation report, in order to probabilistically check the invalidation of caches. Furthermore, we propose three broadcast scheduling methods that are intended to achieve flexible broadcasting structured by the Bloom filter: fragmentation avoidance scheduling method (FASM), metrics balancing scheduling method (MBSM), and minimizing access time scheduling method (MASM). The broadcast schedule is arranged for consecutive accesses to geographically neighboring invalidation reports. In addition, the effectiveness of the proposed methods is evaluated by simulation. The results indicate that the MBSM and MASM achieve a high rate of performance scheduling. Compared to the FASM, the MBSM reduces the access time by 34%, while the fragmentations on the resultant schedule increase by 40%, and the MASM reduces the access time by 40%, along with an 85% increase in the number of fragmentations.

In this paper, we propose a preemptive priority handoff scheme for integrated voice/data cellular mobile systems. In our scheme, calls are divided into three different classes: handoff voice calls, originating voice calls, and data calls. In each cell of the system there is a queue only for data calls. Priority is given to handoff voice calls over the other two kinds of calls. That is, the right to preempt the service of data is given to a handoff voice call if on arrival it finds no idle channels. The interrupted data call returns to the queue. The system is modeled by a two-dimensional Markov chain. We apply the Successive Over-Relaxation (SOR) method to obtain the equilibrium state probabilities. Blocking and forced termination probabilities for voice calls are obtained. Moreover, average queue length and average transmission delay of data calls are evaluated. The results are compared with another handoff scheme for integrated voice/data cellular mobile systems where some numbers of channels are reserved for voice handoff calls. It is shown that, when the data traffic is not very light, the new scheme can provide lower blocking probability for originating voice calls, lower forced termination probability for ongoing voice calls, and shorter average queue length and less average transmission delay for data calls.

In this paper, we propose DSVMA (Data Steal into Voice Multiple Access) scheme for integration of voice and data in wireless information networks. By using speech activity detectors and effective downstream control signals, DSVMA enables data terminals to transmit multi-packet messages when voice terminals are in silent periods. The S-G (throughput versus offered load) performance of the DSVMA system and the blocking probabilities of both the second generation systems and the DSVMA systems are evaluated by the static analysis. A dynamic analysis of a system with finite number of terminals is also presented using an approximate Markov analysis method. Some numerical examples are given in the paper. As a result, it is shown that DSVMA can improve the channel utility efficiency of a circuit-switched TDMA (Time Division Multiple Access) wireless communication system and is directly applicable for second generation wireless information systems.

In this paper, we propose an analytic model using a semi-markov process for parallel computers which provides hardware support for a cache coherence mechanism. The model proposed here, the Semi-markov Memory and Cache coherence Interference model, can be used for the performance prediction of cache coherence based parallel computers since it can be easily applied to descriptions of the waiting states due to network contention or memory interference of both normal data accesses and cache coherence requests. Conventional analytic models using stochastic processes to describe parallel computers have the problem of numerical explosion in the number of states necessary as the system size increases even for simple parallel computers without cache coherence mechanisms. The number of states required by constructing our proposing analytic model, however, does not depend on the system size but only on the kind of cache coherence protocol. For example, the number of states for the Synapse cache coherence protocol is only 20, as is described in this paper. Using the proposed analytic model, we investigate several comparative experiments with widely known simulation results. We found that there is only a 7.08% difference between the simulation and our analytic model, while our analytic model can predict the performance of a 1,024 processor system in the order of microseconds.

In this paper, we apply the Semi-markov Memory and Cache coherence Interference (SMCI) model, which we had proposed for invalidating based cache coherent parallel computers, to an updating based protocol. The model proposed here, the SMCI/Dragon model, can predict performance of cache coherent parallel computers with the Dragon protocol as well as the original SMCI model for the Synapse protocol. Conventional analytic models by stochastic processes to describe parallel computers have the problem of numerical explosion in the number of states necessary as the system size increases. We have already shown that the SMCI model achieved both the small number of states to describe parallel computers with the Synapse protocol and the inexpensive computation cost to predict their performance. In this paper, we demonstrate generality of the SMCI model by applying it to the another cache coherence protocol, Dragon, which has opposite characteristics than Synapse. We show the number of states required by constructing the SMCI/Dragon model is only 21 which is as small as SMCI/Synapse, and the computation cost is also the order of microseconds. Using the SMCI/Dragon model, we investigate several comparative experiments with widely known simulation results. We found that there is only a 5. 4% differences between the simulation and the SMCI/Dragon model.

A new type of Meteor Burst Communication (MBC) network is developed. Each unit of the network is based on a DSP board running a modem software. All the fundamental blocks and functions of a modem are implemented in software. Unlike hardware modems, this software modem has flexibility of system configuration and operation. The system implements adaptability in terms of modulation type (number of phases in MPSK) using a unique dynamic channel estimation scheme appropriate for MBC channel. An MBC network protocol is implemented within the modem software. Some preliminary experiments were carried out for differential BPSK and differential QPSK modulations over a practical meteor burst link, and the results are presented.

This paper presents a queueing system with a load balancing mechanism and an approximate model. We can get the utilization of servers and the distribution ratio from the model. The values agree well the results of simulations.

In ad-hoc on-demand routing algorithm, when a route is broken a relay node must perform error transaction and the source node must do rerouting to discover an alternate route. It is important to construct a stable route when route discovery occurs. In this paper, we use relative speeds among nodes as a measure of node mobility. Our routing algorithm chooses nodes of lower relative speed as relay nodes. As a result of our simulation, when there is one session in the network, our proposing algorithm can reduce the number of route breaks: about 3 times smaller than DSR. And our proposing algorithm can deliver more packets than DSR: 18% higher rate. However, in the congested traffic situation our algorithm should be improved.

In OLSR (Optimized Link State Routing Protocol), the multipoint relay mechanism has been introduced to minimize routing overhead for flooding control traffic. In order to achieve as low a routing overhead as possible, the selection of MPRs (multipoint relays) is designed to limit the overall number of such relays in the network. OLSR provides the shortest paths in terms of hops; however, it does not take into account the QoS (quality of service) requirements. Therefore, QOLSR (Quality OLSR), which adds a QoS extension to the OLSR, has been proposed. Although QOLSR provides the best QoS path, its selection process does not consider the number of MPRs, which causes an increase in the routing overhead. In this paper, we focus on the selection process of MPRs in link state QoS routing protocol. We propose three heuristics for high-efficiency selections: MIMS, MQES, and MCIS. The basic approach of these selections is to determine a smaller set of MPRs that provide better QoS paths between any two nodes. The main objective in doing so is to maximize the QoS effect while limiting the routing overhead. In addition, we evaluate the performance of the routing protocols with the proposed selections by simulation. The results indicate that MIMS and MCIS achieve high-efficiency selection; as compared to QOLSR, MIMS reduces the maintenance cost by 30%, while the throughput of the resultant path is decreased by 13%, and MCIS reduces the cost by 21% without any decrease in the throughput.

A critical problem with wireless LAN-based positioning systems is the degradation in position estimation accuracy due to complex variation in the strength of the received signal, which originates in the nature of the underlying wireless channel. Handling such variation effectively is essential for the creation of practical wireless LAN-based positioning systems. In this paper, we propose a collaborative mechanism for correcting position estimation errors. The main objective is to assist users in correcting estimation errors manually by providing access to a shared body of accumulated information on corrections made by many other users. In particular, the mechanism is designed to enable any group of users to collaboratively build upon this body of information. Finally, we evaluate the effectiveness of the proposed mechanism through experiments. The results confirm that the proposed mechanism can provide effective estimation error correction in a realistic environment.

This paper presents a variable rate transmission scheme suitable for bandlimited meteor burst channel. Meteor Burst Communication (MBC) is a unique type of radio communication, which is primarily used for non-realtime remote data collection. In the paper, along with conventional BPSK and QPSK modulations, QAM and M-ary Bi-orthogonal modulations are analyzed for software modem implementation in an MBC system. Performance of the modulation methods is presented for both static AWGN channel and meteor burst channel. The proposed scheme for variable rate transmission dynamically estimates the MBC channel and varies the modulation type of a software modem, to control the transmission rate between bursts. The scheme dynamically selects a modulation type and packet length that will maximize the average throughput of the system. Performance of the scheme is analyzed and compared with conventional fixed rate modems. A practical implementation for software modem is suggested that uses a common core modulator/demodulator structure.

In our preceding paper, I-ISMA (Idle Signal Multiple Access for Integrated services), a combination of ISMA and time reservation technique, was proposed to transmit an integrated voice and data traffic in third generation wireless communication networks. There, the channel capacity of I-ISMA was evaluated by the static analysis. To fully estimate performance of contention-based channel access protocols, however, we also need dynamic analysis to evaluate stability, delay, etc. Particularly, in systems concerning real-time voice transmission, delay is one of the most important performance measures. A six-mode model to describe an I-ISMA system is set up. With some assumptions for simplification, the dynamic behavior of the system is approximated by a Markov process so that the EPA (Equilibrium Point Analysis), a fluid approximation method, can be applied to the analysis. Then, numerical and simulation results are obtained for some examples. By means of the same analysis method and under the same conditions, the performance of PRMA is evaluated and compared briefly with that of I-ISMA.

This paper deals with the method of integration of voice and data in wireless communication systems. By applying the DSV (Data Steal into Voice) technique to D-TDMA (Dynamic Time Division Multiple Access) systems, this paper presents an MAC (Media Access Control) method of integration of voice and data for the systems such as cellular radios and cordless phones. After a brief review of the D-TDMA scheme and the DSV technique, the protocol called D-TDMA/DSV is described. Then, a static analysis to derive the channel capacity and a dynamic analysis to evaluate the throughput and delay performance are presented. An extension of TFA (Transient Fluid Approximation) analysis is employed in the dynamic analysis. With the same system parameters, the capacity of D-TDMA/DSV is compared with that of the traditional D-TDMA. Under the limitation of the blocking probability required for cellular radios, some numerical examples of dynamic analysis are given to show the throughput and delay performance of the system.

It is expected that software receivers will be widely available for radio communication, broadcasting and radio monitoring applications because they are able to be equipped with multimode, multirate and multiband functions in a single hardware platform. This paper describes the basic techniques required for software receivers for both hardware and software. The evaluation items and methods were studied and some evaluations done with an experimental software receiver model fabricated for radio monitoring applications. Future concepts in radio communication, broadcasting and radio monitoring applications where software receivers are thought to be suitable, were studied, and problems for realization identified.

Corresponding to the development of B-ISDN, integrated services for data, voice, etc. are imperatively required for the so called third generation wireless communication networks. In this paper, I-ISMA (Idle Signal Multiple Access for Integrated services) is proposed to transmit integrated voice and data traffic from dispersed terminals to a base station. In the system, data packets and the first packets of talkspurts of conversational speeches are transmitted using ISMA protocol over a shared channel while subsequent packets of talkspurts are sent with time reservation technique. The channel capacity of I-ISMA is evaluated and compared with that of PRMA. The region in which I-ISMA has larger capacity than PRMA is figured out. Generally speaking, I-ISMA has larger capacity than PRMA when the duration for transmitting and detecting an idle signal is not too long and the channel is not too congested by the reserved voice transmissions. When we concern real time voice transmission, delay is one of the most important performance measures. Only is a qualitative discussion on delay performance given here. The quantitative evaluation is obtained by the dynamic analysis in our succeeding paper.

The M(m)/M/K and M(m)/M/ models with synchronous fluctuation of traffic intensity are considered. The phase process is assumed to make changes according to an irreducible m-phase Markov chain. In contrast to the model with asynchronous fluctuation of parameters, phase changes may occur in synchronization with an arrival or beginning of a customer's service. We study mainly the steady-state regime of our models, and observe that, in general, closed form solutions for the limiting probabilities are difficult to obtain but their numerical computation is rather straightforward. We give a necessary and sufficient condition for the steady-state to be attained. For the model M(m)/M/K, it is shown that, for the case where the traffic intensity of one phase is greater than one (even if the average traffic intensity is less than one) the average queue length approaches infinity as the fluctuations among phases gets more sluggish. However, for the case where the traffic intensity for all phases is less than one, the queue length is moderate and not dependent as much on the rate of fluctuation among phases. Numerical examples are given and discussed. Finally, we point out that, our models may be more tractable than the asynchronous ones, when we try to generalize them to the case of general inter-arrival, service, or sojourn time distribution.

In December 2001, the authors started two kinds of experiments on the meteor burst communication (MBC) in Antarctica to study the ability of MBC as a communication medium for data collection systems in that region. In the first experiment, a continuous tone signal is transmitted from Zhongshan Station. The signal received at Syowa Station (about 1,400 km apart) is recorded and analyzed. This experiment is aimed to study basic properties of the meteor burst channel in that high latitude region. On the other hand, the second experiment is designed to estimate data throughput of a commercial MBC system in that region. A remote station at Zhongshan Station tries to transfer data packets each consisting of 10 data words to the master station at Syowa Station. Data packets are generated with five minutes interval. In this paper, we explain the experiments, briefly examine the results of the first year (from April 2002 to March 2003), and put forward the plan for the experiments in the second and third year. From the data available thus far, we can see that 1) the sinusoidal daily variation in the meteor activity typical in middle and low latitude regions can not be clearly seen, 2) non-meteoric propagations frequently dominate the channel especially during night hours, 3) about 60% of the generated data packets are successfully transferred to the master station within two hours delay even though we are now operating the data transfer system only for five minutes in each ten minutes interval, etc.