As a variety of digital services are provided through networks, more and more efforts are made to ensure dependability of software behavior implementing services. Formal methods and tools have been considered as promising means to support dependability in complex software systems during the development. On the other hand, there have been serious doubts on practical applicability of formal methods. This paper overviews the present state of formal methods and discusses their applicability, especially focusing on two representative methods (SPIN and B Method) and their recent industrial applications. This paper also discusses applications of formal methods to dependable networked software.

This paper studies nonlinear dynamics of a simplified model of multiple-input parallel buck converters. The dynamic winner-take-all switching is used to achieve N-phase synchronization automatically, however, as parameters vary, the synchronization bifurcates to a variety of periodic/chaotic phenomena. In order to analyze system dynamics we adopt a simple piecewise constant modeling, extract essential parameters in a dimensionless circuit equation and derive a hybrid return map. We then investigate typical bifurcation phenomena relating to N-phase synchronization, hyperchaos, complicated superstable behavior and so on. Ripple characteristics are also investigated.

A low power consumption 16-bit fixed point Digital Signal Processor (DSP) has been developed to realize a half-rate CODEC for the Personal Digital Cellular (PDC) system. Dual datapath architecture has been employed to execute multiply-accumulate (MAC) operations with a high degree of efficiency. With this architecture. 86.3% of total MAC operations in the Pitch Synchronous Innovation Code Excited Linear Prediction (PSI-CELP) program are executed in parallel, so that total instruction cycles are reduced by 23.1%. The area overhead for the dual datapath architecture is only 3.0% of the total area. Furthermore, in order to reduce power consumption, circuit design techniques are also extensively applied to RAMs. ROMs, and clock circuits, which consume the great majority of power. By reducing the number of precharging bit lines, a power reduction of 49.8% is achieved in RAMs, and above 40% in ROMs. By applying gated clock to clock lines, a power reduction of 5.0% is achieved in the DSP that performs the PSI-CELP algorithm. The DSP is fabricated in 0.5 µm single-poly, double-metal CMOS technology. The PSI-CELP algorithm for the PDC half-rate CODEC can operate at 22.5 MHz instruction frequency and 1.6 V supply voltage. resulting in a low-power consumption of 28 mW.

In orthogonal frequency division multiplexing (OFDM) system, a guard interval (GI) is used to remove the inter-symbol interference (ISI) due to a multipath channel. It is difficult to set an optimal GI length in the environment whose multipath varies. In this paper, we propose a variable guard interval based on the estimated maximum delay of a multipath channel. The maximum delay is estimated from a channel impulse response (CIR), which is estimated by a preamble symbol. However, since the estimated CIR includes the noise, it is difficult to decide the optimal GI. In order to solve the problem, we introduce the method which selects the path whose signal to noise ratio is high. Additionally, the information of the optimal GI length is required to be transmitted from a receiver to a transmitter. In this paper, we use an acknowledgment (ACK) frame for the feedback of the GI information.

In this paper, we propose a power-efficient LDPC decoder architecture based on an accelerated message-passing schedule. The proposed decoder architecture is characterized as follows: (i) Partitioning a pipelined operation not to read and write intermediate messages simultaneously enables the accelerated message-passing schedule to be implemented with single-port SRAMs. (ii) FIFO-based buffering reduces the number of SRAM banks and words of the LDPC decoder based on the accelerated message-passing schedule. The proposed LDPC decoder keeps a single message for each non-zero bit in a parity check matrix as well as a classical schedule while achieving the accelerated message-passing schedule. Implementation results in 0.18 [µm] CMOS technology show that the proposed decoder architecture reduces an area of the LDPC decoder by 43% and a power dissipation by 29% compared to the conventional architecture based on the accelerated message-passing schedule.

Room temperature cw operation of transverse mode stabilized 680-nm InGaAIP laser diodes have been achieved for the first time. A self-aligned structure was fabricated by two-step metalorganic chemical vapor deposition, which included the selective growth technique.

A new switches-capacitor immittance converter (SCIC) circuit based on the bilinear transformation is propose. The inductive (n+1)-terminal network is realized using in SCIC's and one capacitive (n+1)-terminal network. The SCIC consists of only one buffer, one op amp and three capacitors.

Mixed-signal LSIs promise to permit increased levels of integration, not only in voiceband but also in multi-GHz-band applications such as wireless communications and optical data links. This paper reviews the evolution of mixed-signal communications LSIs and discusses some of their design problems, including device noise and crosstalk noise. In the low-power and low-voltage designs emerging as new disciplines, the target supply voltage for voiceband LSIs is around 1 V, and even GHz-band circuits are approaching 2 V. MOS devices are expected to play an important role even in the frequency range over 100 MHz, in the area of wireless or optical communications circuits.

How to minimize the number of mirroring resources under a QoS constraint (resource minimization problem) is an important issue in content delivery networks. This paper proposes a novel approach that takes advantage of the parallelism of dynamically reconfigurable processors (DRPs) to solve the resource minimization problem, which is NP-hard. Our proposal obtains the optimal solution by running an exhaustive search algorithm suitable for DRP. Greedy algorithms, which have been widely studied for tackling the resource minimization problem, cannot always obtain the optimal solution. The proposed method is implemented on an actual DRP and in experiments reduces the execution time by a factor of 40 compared to the conventional exhaustive search algorithm on a Pentium 4 (2.8 GHz).

This paper presents a precise characterization of high-frequency characteristics of intrinsic channel of FinFET. For the de-embedding of the parasitics attached to the source, drain and gate terminals, it proposes special calibration patterns which can place the reference surface just beside the intrinsic part of the FinFET. It compares the measured S parameter data up to 40 GHz with the device simulation and shows good matching. The experimental data of the through pattern also confirms the accuracy of the de-embedded parasitics and extracted intrinsic part of FinFET.

This paper proposes a consensus-based distributed Particle Swarm Optimization (PSO) algorithm with event-triggered communications for a non-convex and non-differentiable optimization problem. We consider a multi-agent system whose local communications among agents are represented by a fixed and connected graph. Each agent has multiple particles as estimated solutions of global optima and updates positions of particles by an average consensus dynamics on an auxiliary variable that accumulates the past information of the own objective function. In contrast to the existing time-triggered approach, the local communications are carried out only when the difference between the current auxiliary variable and the variable at the last communication exceeds a threshold. We show that the global best can be estimated in a distributed way by the proposed event-triggered PSO algorithm under a diminishing condition of the threshold for the trigger condition.

Recommender System (RS) predicts user's ratings towards items, and then recommends highly-predicted items to user. In recent years, RS has been playing more and more important role in the agent research field. There have been a great deal of researches trying to apply agent technology to RS. Collaborative Filtering, one of the most widely used approach to predict user's ratings in Recommender System, predicts a user's rating towards an item by aggregating ratings given by users who have similar preference to that user. In existing approaches, user similarity is often computed on the whole set of items. However, because the number of items is often very large and so is the diversity among items, users who have similar preference in one category may have totally different judgement on items of another kind. In order to deal with this problem, we propose a method to cluster items, so that inside a cluster, similarity between users does not change significantly from item to item. After the item clustering phase, when predicting rating of a user towards an item, we only aggregate ratings of users who have similarity preference to that user inside the cluster of that item. Experiments evaluating our approach are carried out on the real dataset taken from MovieLens, a movies recommendation web site. Experiment results suggest that our approach can improve prediction accuracy compared to existing approaches.

Thermal properties of InGaAlP laser diodes have been analyzed by computer simulation. Self-consistent analysis considering heat conduction, current distribution and optical waveguide mode has made it clear that there exist optimum structural parameters minimizing the threshold current.

A 2-GHz monolithic Si-bipolar logarithmic/ limiting amplifier is described. It features a waveform-dependent current phase shifter that compensates for the intrinsic dependence of unit-amplifier phase shifts on input signal amplitudes and layout techniques that minimize crosstalk in Si substrate. The amplifier dissipates 250 mW at a 3-V supply, which is less than 1/4 of that of previously reported ICs. The dynamic range of a received signal strength indicator (RSSI) is 60 dB and the limited-output phase deviation is less than 7 deg. at 2 GHz. Therefore, this amplifier is quite suitable for single-conversion transceivers for broadband wireless access systems.

Test coverage is an important indicator of whether software has been sufficiently tested. However, there are several problems with the existing measurement tools for test coverage, such as their cost of development and maintenance, inconsistency, and inflexibility in measurement. We propose a consistent and flexible measurement framework for test coverage that we call the Open Code Coverage Framework (OCCF). It supports multiple programming languages by extracting the commonalities from multiple programming languages using an abstract syntax tree to help in the development of the measurement tools for the test coverage of new programming languages. OCCF allows users to add programming language support independently of the test-coverage-criteria and also to add test-coverage-criteria support independently of programming languages in order to take consistent measurements in each programming language. Moreover, OCCF provides two methods for changin the measurement range and elements using XPath and adding user code in order to make more flexible measurements. We implemented a sample tool for C, Java, and Python using OCCF. OCCF can measure four test-coverage-criteria. We also confirmed that OCCF can support C#, Ruby, JavaScript, and Lua. Moreover, we reduced the lines of code (LOCs) required to implement measurement tools for test coverage by approximately 90% and the time to implement a new test-coverage-criterion by over 80% in an experiment that compared OCCF with the conventional non-framework-based tools.

In this paper, we propose a partially-parallel LDPC decoder which achieves a high-efficiency message-passing schedule. The proposed LDPC decoder is characterized as follows: (i) The column operations follow the row operations in a pipelined architecture to ensure that the row and column operations are performed concurrently. (ii) The proposed parallel pipelined bit functional unit enables the column operation module to compute every message in each bit node which is updated by the row operations. These column operations can be performed without extending the single iterative decoding delay when the row and column operations are performed concurrently. Therefore, the proposed decoder performs the column operations more frequently in a single iterative decoding, and achieves a high-efficiency message-passing schedule within the limited decoding delay time. Hardware implementation on an FPGA and simulation results show that the proposed partially-parallel LDPC decoder improves the decoding throughput and bit error performance with a small hardware overhead.

This paper studies two kinds of simple switched dynamical systems with piecewise constant characteristics. The first one is based on the single buck converter whose periodic/chaotic dynamics are analyzed precisely using the piecewise linear phase map. The second one is based on a paralleled system of the buck converters for lower voltages with higher current capabilities. Referring to the results of the single system, it is clarified that stable multi-phase synchronization is always possible by the proper use of the switching strategies and adjustment of the clock period. Presenting a simple test circuit, typical operations are confirmed experimentally.

In this paper, we propose a distributed subgradient-based method over quantized and event-triggered communication networks for constrained convex optimization. In the proposed method, each agent sends the quantized state to the neighbor agents only at its trigger times through the dynamic encoding and decoding scheme. After the quantized and event-triggered information exchanges, each agent locally updates its state by a consensus-based subgradient algorithm. We show a sufficient condition for convergence under summability conditions of a diminishing step-size.

This paper describes a high-performance, low-power, mixed-signal Digital Signal Processor (DSP) and its application to a single-chip Vector Sum Excited Linear Prediction (VSELP) speech codec. The DSP consists of a 25MIPS, 24bit floating point core-DSP; 13bit oversampling ADC/DAC; 6 KW data ROM; and 3.5 KW data RAM. The total transistor counts of the DSP is 1.3 million and its chip size is 11.0 mm15.8 mm. Unique design techniques are used to reduce the power dissipation, such as the programmable machine cycle time control and the clock supply control scheme in the core-DSP, the address detection for on-chip data ROM/RAM, and the shared-hardware design for digital filters of ADC and DAC. As an application of the DSP, the VSELP speech codec, which is the standard speech codec for the North American and Japanese digital cellular telephone system, has been implemented in a single-chip. Owing ti the salient architecture design and the program optimization techniques, sufficient quality was obtained in the codec at performance of 16.4 MIPS with low-power dissipation of 490 mW.