This paper describes a new method for verifying designs at the RTL with respect to their specifications at the functional level. The base of the verification method shown here is the translation of the specification and design representations to graph models, where the descriptions common to both representations have a symbolic representation. These symbol labeled graphs are then simplified and, by solving the all node-pair path expression problem for them, a pair of regular expressions is obtained for every two nodes in the graphs. The first regular expression in each pair represents the flow of control and the second one the flow of data between the corresponding nodes. The process of verification is carried out by checking whether or not every pair of regular expressions of the specification has a corresponding pair in the design.

The paper considers the design of two families of binary block codes developed for controlling large numbers of errors which may occur in LSI, optical disks and other devices. The semidistance codes are capable of assuring a required signal-to-noise ratio in information retrieval; the t-symmetric error correcting/all unidirectional error detecting" (t-SyEC/AUED) codes are capable of correcting t or fewer symmetric errors and also detecting any number of unidirectional errors caused by the asymmetric nature of transmission or storage madia. The paper establishes an equivalence between these families of codes, and proposes improved methods for constructing, for any values of t, a class of nonsystematic constant weight codes as well as a class of systematic codes. The constructed codes of both classes are shown to be optimal when t is O, and of asymptotically optimal order" in general cases. The number of redundant bits of the obtained nonsystematic code is of the order of (t+1/2)log2 K bits, where K is the amount of information encoded. The obtained systematic codes have redundancy of the order of (t+1)log2 K bits.

Many practical communication protocols provide priority service as well as ordinary service. In such a protocol, the protocol machines can initiate a priority service at most of the states. This characteristic leads an extreme increment of the number of state transitions on the protocol machines and causes state space explosion in verification of safety property of the protocol. This paper describes a method of constructing a communication protocol from composition of a subprotocol for ordinary service and that for priority service. This paper also presents a sufficient condition for a composed protocol to inherit safety property from the subprotocols. By using the composition method and the sufficient condition, the decision problem for safety property of the composed protocol can be reduced to those of the subprotocols. An experimental result of verification of a part of OSI session protocol is also described. The result shows that the method can reduce the computation time for verifying safety property to about 3% against the naive way.

In order to make the implementation of network components flexible and cost effective, it is required to use widely available technologies as the implementation platform. The distributed operating systems can be adopted as such a platform, because they allow to implement a network component using multiple computers connected through a local area network. In this paper, we focus on the Intelligent Network (IN) whose network components are modelled as Functional Entities (FEs), and describe an implementation method of FEs using distributed operating systems. Our method is summarized as follows: The remote procedure call (RPC) is used for the access transparent inter-process communication. The lightweight process mechanism is used for handling concurrent requests. CCF/SSF (Call Control Function/Service Control Function) and SDF (Service Data Function) are implemented as an SSF server and an SDF server, respectively. SCF (Service Control Function) is composed of a Service Dispatcher and a set of Service Executors. The Service Dispatcher accepts all the requests for IN call processing and dispatches them to appropriate Service Executors. Service Executors are created for the individual IN services and execute the service logics. SDF server and Service Executor may be replicated for load partitioning.This paper has also described the implementation of experimental system supporting "Freephone" service based on our method, and showed the performance evaluation of the experimental system in terms of the real-time and concurrent call processing of IN services. We used Mach and SUN OS as a platform for implementing the servers for FEs. The experimental system using four workstations shows that it can handle up to 170IN calls in one second with the additional response time of less than 200msec, which is small enough compared with the response time for the basic connection control. Those results prove that our method is feasible for implementing practical FEs.

This paper proposes a test case generation method for testing concurrent programs as a black box. Typical applications are system testing for switching systems and inter-operability testing for OSI products. We adopt a two-step approach: first generate the control flow graph which represents global behaviors of a given concurrent program, and then apply conventional test case generation methods for the control flow graph. To generate a control flow graph without state space explosion, the black-box equivalence between system behaviors is introduced. The proposed algorithm generates a minimal control flow graph which consists of representatives of equivalence classes. Two practical techniques for the second step are discussed for a case study using a commercial digital PBX. The results show the feasibility of the proposed method.

An improved array architecture to realize fast access, low power dissipation, and wide operating margin, for the 16 Mbit DRAM is proposed. A high speed access is obtained by the fully embedded sense drive scheme for the RAS access time (tRAC), and the special page mode with the hierarchical I/O data bus lines and multi-purpose-register (MPR) for the column address access time (tCAA). A low power dissipation and wide operating margin are obtained by the improved twisted-bit-line (TBL) architecture with double dummy canceling. The 16 Mb DRAM using these architectures has 38 ns tRAC, 14 ns tCAA and 75 mA power dissipation at the typical condition.

This paper describes MENDELS ZONE, a Petri-net-based concurrent programming environment, which is especially suitable for cooperating discrete event systems. MENDELS ZONE adopts MENDEL net, which is a type of high level (hierarchical colored) Petri net. One of the characteristics of the MENDEL nets is a process-oriented hierarchy like CCS, which is different from the subnet-oriented hierarchy in the Jensen's hierarchical colored Petri net. In a process-oriented hierarchy, a hierarchical unit is a process, which is more natural for cooperating and decentralized discrete event control systems. This paper also proposes a design methodology for MENDEL nets. Although many Petri net tools have been proposed, most tools support only drawing, simulation, and analysis of Petri nets; few tools support the design methodology for Petri nets. While Petri nets are good final design documents easy to understand, analyzable, and executable it is often difficult to write Petri nets directly in an earlier design phase when the system structure is obscure. A proposed design methodology makes a designer to construct MENDEL nets systematically using causality matrices and temporal logic. Furthemore, constructed MENDEL nets can be automatically compiled into a concurrent programming language and executed on a parallel computer.

Although individual segments of a natural language such as words have different importance on human interpretation of the meaning, every segment has been uniformly protected by an error-correcting code. If the importance of individual segments is defined by considering their meaning in the sentence, we can adaptively control the level of error-protection for each segment according to its importance in order to reduce errors on human interpretation of the meaning. In this paper, we propose an error-control scheme based on the varying importance of each word. We first introduce a method which determines the importance of each word and then propose an error-control scheme in which several error-correcting codes are alternately used to protect each word according to its importance. Probablity of semantic errors, that is, errors on human interpretation of the meaning, is defined and used as a criterion in mapping error-correcting codes to words possessing different importance. We theoretically formalize the problem of obtaining an optimum mapping which minimizes the probability of semantic errors under some constraint. Given a certain probability distribution of the importance of words and set of error-correcting codes, we can derive the optimum mapping. The proposed error-controlling scheme is theoretically evaluated by comparing its probability of semantic errors with that of a conventional scheme in which every word is uniformly protected by a single error-correcting code. Results show that the proposed scheme can considerably raduce the probability of semantic errors while retaining the same average transmission rate or redundancy.

This letter proposes an improvement of the equivalent source method in order to give an accurate solution for the scattering of an electromagnetic plane wave by a conducting cylinder with edges.

This letter considers a subclass of t-symmetric error correcting/all unidirectional error detecting (t-SyEC/AUED) codes in which the information is represented in an m-out-of-k coded form, which thus can be regarded as virtually systematic for practical purposes. For t3, previous researchers proposed methods for constructing codes of this subclass which are either optimal or of asymptotically optimal order. This letter proposes a new method for constructing, for any values of t, m and k, codes that are either optimal or of asymptotically optimal order. The redundancy of the obtained code is of the order tlog2k bits when mt.

This paper describes a new metric for evaluating the cost effectiveness of software reviews. The proposed metric is based on the degree to which costs needed for detecting all faults from software are reduced by software reviews in a project. The metric can be interpreted as combining two conventional metrics proposed by Fagan (1976) and Collofello and Woodfield (1989). As the proposed metric is normalized by virtual testing cost, we can compare the values of it among any different kind of projects. Using an experimental evaluation of the conventional metrics and the proposed metric for data collected in an industrial environment, we show the validity and usefulness of the proposed metric. In addition, we present a method to estimate a value of the proposed metric by using only the values which can be computed during the software reviews.

Isotope dilution secondary ion mass spectroscopy (ID-SIMS) using 30Si as a spike is investigated as a quantitative analysis method for trace amounts of Si. For a standard solution of Si, the relateve standard deviation of results using this method is 5% for 0.2 µg Si, and the determination lower limit is 18 ng. Using this method, the amount of Si deposited on the Ge(100) surface by the self-limited adsorption of SiH2Cl2 is determined to be about 1.00.2 monolayer.

The mechanisms for executing concurrent applications proposed so far fall into one of three groups: processes, kernel-level threads, and user-level threads. Each of them is insufficient in terms of either parallelism, the flexibility to combine separately developed programs at run-time, or costs of operations such as creation, switching, and termination. A thread facility in the XERO operating system overcomes this problem and provides a uniform framework for executing concurrent applications. To achieve parallelism of threads, the flexibility to combine separately developed programs at run-time, and fast thread operations, the operating system kernel and a thread management module in a user address space manage threads cooperatively. We implemented the cooperative thread management mechanism and measured its performance to examine the effectiveness of our approach.

Low temperature experiments have been made to demonstrate the operation of LiNbO3 optical modulator with superconducting electrodes. The operation of the modulator for applied dc signals as well as microwave signals in the frequency range between 8 GHz and 12 GHz has been observed at temparatures as low as 4.2 K. The present results indicate a possibility of realizing high performance LiNbO3 optical modulators employing superconducting electrodes.

Weather conditions affect the performance of satellite broadcasting receiving systems. For example, snow accretion on antennas degrades G/T seriously because it reduces received signal power and also can increase antenna noise. We need a continuous measurement of G/T to evaluate the effect of the weather conditions to the satellite broadcasting receiving systems. However, a conventional method cannot perform the continuous measurement because the antenna under test must be oriented in a specific direction (to the zenith) to obtain a noise level in a satellite broadcasting channel. This paper presents the continuous measurement of G/T for the satellite broadcasting receiving systems. We describe details of the measurement method. In our measurement system, a standard antenna is placed at the inside of a room in order to prevent the weather conditions from affecting the gain of the standard antenna. The power flux density at the inside of the room is different from that at the outside where the antennas under test are placed. Employing the effective gain of the standard antenna, we take the difference of the power flux density into account. Moreover, we propose a method to estimate the noise level in the satellite broadcasting channel from the values at the outside of the channel, and clarify the accuracy of the noise estimation. Then, we show measurement results of the G/T values for several receiving systems. From these results, we show that the G/T measurement system has high precision. Also, from the specifications of the antenna gain and typical values of the noise figure, it is expected that the measurement system has a sufficient accuracy.

This paper describes the structure and properties of superconductive small antennas with thin-film matching circuits. These circuits make it possible to realize small antennas, 38 mm20 mm16 mm in size. This is one quarter the length of our previously reported ceramic antennas. The actual gain of this antennas was -4.5 dBi at 470 MHz. This value is 5.5 dB higher than that of Cu antennas with exactly the same structure.

We have fabricated superconducting microwave passive components such as resonators, bandpass filters and delay lines with YBCO thin film conductors deposited on MgO substrates. Considerably high unloaded Q values of 12000 at 5.5 GHz was obtained with the YBCO microstrip resonator at 77 K, which indicated that the surface resistance of the YBCO thin film was 0.79 mΩ at that frequency and temperature. Excellent microwave properties were also demonstrated with the bandpass filter and the delay line. Considerably low insertion loss of about 1 dB was obtained with the 10 GHz YBCO bandpass filters at 77 K which have a various bandwidth from 0.5% to 10%. Also excellent microwave propagation was obtained with a 1.3 nsec YBCO coplanar delay line. Its insertion loss was less than 1 dB for the frequencies up to 4 GHz.

An integrated multiplexer in intermediate node is analyzed. The multiplexer is modeled as a system with multiple synchronous servers (channels) and having two kinds of customers. Between the two, one is wideband (WB) and the other is narrowband (NB); they are queueable with the same deterministic service time. The WB customer is given higher priority of channel access than the NB. To incorporate the delay constraint of WB, we use a simple instant discarding scheme for WB. As a result, the system states defined just after the beginning of a slot form an one-dimensional embedded Markov chain. This makes the analysis computationally tractable. The performance measures such as queue length distribution, average blocking probability, and average waiting time are obtained, particularly, the waiting time distribution. Some interesting numerical examples are discussed. Simulation results are also provided to help verify the validity of analysis.

Based on the Fornasini-Marchesini second local state-space (LSS) model, the coefficient sensitivities of two-dimensional (2-D) digital filters are analyzed in conjunction with frequency weighting functions. The overall sensitivity called the frequency-weighting sensitivity is then evaluated using the 2-D generalized Gramians that are newly introduced for the Fornasini-Marchesini second LSS model. Next, the 2-D filter structures that minimize the frequency-weighting sensitivity are synthesized for two cases of no constraint and scaling constraints on the state variables. Finally, an example is given to illustrate the utility of the proposed technique.

In this letter, we consider a magnetic or optical recording system employing a concatenated code that consists of a runlength-limited (d, k) block code as an inner code and a byte-error-correcting code as an outer code. (d, k) means that any two consecutive ones in the code bit stream are separated by at least d zeros and by at most k zeros. The minimum separation d and the maximum separation k are imposed in order to reduce intersymbol interference and extract clock control from the received bit stream, respectively. This letter recommends to use as the outer code a unidirectional-byte-error-correcting code instead of an ordinary byte-error-correcting code. If we devise the mapping of the code symbols of the outer code onto the codewords of the inner code, we may improve the error performance. Examples of the mappings are described.