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.

As pervasive computing technologies develop fast, the privacy protection becomes a crucial issue and needs to be coped with very carefully. Typically, it is difficult to efficiently identify and manage plenty of the low-cost pervasive devices like Radio Frequency Identification Devices (RFID), without leaking any privacy information. In particular, the attacker may not only eavesdrop the communication in a passive way, but also mount an active attack to ask queries adaptively, which is obviously more dangerous. Towards settling this problem, in this paper, we propose two lightweight authentication protocols which are privacy-preserving against active attack, in an asymmetric way. That asymmetric style with privacy-oriented simplification succeeds to reduce the load of low-cost devices and drastically decrease the computation cost for the management of server. This is because that, unlike the usual management of the identities, our approach does not require any synchronization nor exhaustive search in the database, which enjoys great convenience in case of a large-scale system. The protocols are based on a fast asymmetric encryption with specialized simplification and only one cryptographic hash function, which consequently assigns an easy work to pervasive devices. Besides, our results do not require the strong assumption of the random oracle.

Previously proposed batch signature schemes do not allow a signer to generate a signature immediately for sequentially asked signing queries. In this letter, we propose flexible batch signatures which do not need any waiting period and have very light computational overhead. Therefore our schemes are well suited for low power devices.

The MIMO system can meet the growing demand for higher capacity in wireless communication fields. So far, the authors have reported that, based on channel measurements, uncoded performance of narrowband MIMO spatial multiplexing in indoor line-of-sight (LOS) environments generally outperforms that in non-LOS (NLOS) ones under the same transmit power condition. In space-frequency coded MIMO-OFDM spatial multiplexing, however, we cannot expect high space-frequency diversity gain in LOS environments because of high fading correlations and low frequency selectivity of channels so that the performance may degrade unlike uncoded cases. In this letter, we present the practical performance of coded MIMO-OFDM spatial multiplexing based on indoor channel measurements. The results show that an LOS environment tends to provide lower space-frequency diversity effect whereas the MIMO-OFDM spatial multiplexing performance is still better in the environment compared with an NLOS environment.

In this letter we propose a simple adaptive algorithm which solves the unit-norm constrained optimization problem. Instead of conventional parameter norm based normalization, the proposed algorithm incorporates single parameter normalization which is computationally much simpler. The simulation results illustrate that the proposed algorithm performs as good as conventional ones while being computationally simpler.

Two variable gain amplifiers (VGAs) that adopt new approximated exponential equations are proposed in this paper. The dB-linear range of the proposed VGAs is extended more than what the approximated exponential equations predict by a bias circuit technique that adopts negative feedback. The proposed VGAs feature wide gain variation, low-power, high linearity, wide control signal range, and small chip size. One of the proposed VGAs is fabricated in 0.18 µm CMOS technology and measurements show a gain variation of 83 dB (-3647 dB) with a gain error of less than 2 dB, and P1 dB/IIP3 from -55/8 to -20/20.5 dBm, while consuming an average current of 3.4 mA from a 1.8 V supply; the chip occupies 0.4 mm2. The other VGA is simulated in 0.18 µm CMOS technology and simulations show a gain variation of 91 dB (-4150 dB), and P1 dB/IIP3 from -50/-25 to -33/0 dBm, while consuming an average current of 1.5 mA from a 1.8 V supply.

This paper presents an asynchronous design technique, an enabler for the emerging technology of flexible microelectronics that feature low-temperature processed polysilicon (LTPS) thin-film transistors (TFT) and surface-free technology by laser annealing/ablation (SUFTLA®). The first design instance chosen is an 8-bit microprocessor. LTPS TFTs are good for realizing displays having integrated VLSI circuit at lower costs. However, LTPS TFTs have drawbacks, including substantial deviations in characteristics and the self-heating phenomenon. To solve these problems, the authors adopted the asynchronous circuit design technique and developed an asynchronous design language called Verilog+, which is based on a subset of Verilog HDL® and includes minimal primitives used for describing the communications between modules, and the dedicated tools including a translator called xlator and a synthesizer called ctrlsyn. The flexible 8-bit microprocessor stably operates at 500 kHz, drawing 180 µA from a 5 V power source. The microprocessor's electromagnetic emissions are 21 dB less than those of the synchronous counterpart.

The computation involved in multiuser detection (MUD) for multicarrier CDMA (MC-CDMA) based on maximum likelihood (ML) principle grows exponentially with the number of users. Particle swarm optimization (PSO) with soft decisions has been proposed to mitigate this problem. The computational complexity of PSO, is comparable with genetic algorithm (GA), but is much less than the optimal ML detector and yet its performance is much better than GA.

An all CMOS variable gain amplifier (VGA) which features wide dB-linear gain range per stage (45 dB), low power consumption (1.32 mW), small chip size (0.13 mm2), and low supply voltage (1.2 V) is described. The dB-linear range is extended by reducing the supply voltage of the conventional V-to-I converter. The two-stage VGA implemented in 0.18 µm CMOS offers 90 dB of gain variation, 3 dB bandwidth of greater than 21 MHz, and max/min input IP3 and P1 dB, respectively, of -5/-42 and -12/-50 dBm.

Efforts have been devoted to maximizing memory array densities. However, as the devices are scaled down in dimension and getting closer to each other, electrical interference phenomena among devices become more prominent. Various features of 3-D memory devices are proposed for the enhancement of memory array density. In this study, we mention 3-D NAND flash memory device having pillar structure as the representative, and investigate the paired cell interference (PCI) which inevitably occurs in the read operation for 3-D memory devices in this feature. Furthermore, criteria for setting up the read operation bias schemes are also examined in existence with PCI.

We propose a new approach to personal identification using derived vectorcardiogram (dVCG). The dVCG was calculated from recorded ECG using inverse Dower transform. Twenty-one features were extracted from the resulting dVCG. To analyze the effect of each feature and to improve efficiency while maintaining the performance, we performed feature selection using the Relief-F algorithm using these 21 features. Each set of the eight highest ranked features and all 21 features were used in SVM learning and in tests, respectively. The classification accuracy using the entire feature set was 99.53 %. However, using only the eight highest ranked features, the classification accuracy was 99.07 %, indicating only a 0.46 % decrease in accuracy compared with the accuracy achieved using the entire feature set. Using only the eight highest ranked features, the conventional ECG method resulted in a 93 % recognition rate, whereas our method achieved >99 % recognition rate, over 6 % higher than the conventional ECG method. Our experiments show that it is possible to perform a personal identification using only eight features extracted from the dVCG.

This paper presents a processor architecture for high-speed and reliable trinocular stereo matching based on adaptive window-size control of SAD (Sum of Absolute Differences) computation. To reduce its computational complexity, SADs are computed using images divided into non-overlapping regions, and the matching result is iteratively refined by reducing a window size. Window-parallel-and-pixel-parallel architecture is also proposed to achieve to fully exploit the potential parallelism of the algorithm. The architecture also reduces the complexity of an interconnection network between memory and functional units based on regularity of reference pixels. The stereo matching processor is designed in a 0.18 µm CMOS technology. The processing time is 83.2 µs@100 MHz. By using optimal scheduling, the increases in area and processing time is only 5% and 3% respectively compared to binocular stereo vision although the computational amount is double.

Further development of a network based on the Inverse Function Delayed (ID) model which can recall temporal sequences of patterns, is proposed. Additional advantage is taken of the negative resistance region of the ID model and its hysteretic properties by widening the negative resistance region and letting the output of the ID neuron be almost instant. Calling this neuron limit ID neuron, a model with limit ID neurons connected pairwise with conventional neurons enlarges the storage capacity and increases it even further by using a weightmatrix that is calculated to guarantee the storage after transforming the sequence of patterns into a linear separation problem. The network's tolerance, or the model's ability to recall a sequence, starting in a pattern with initial distortion is also investigated and by choosing a suitable value for the output delay of the conventional neuron, the distortion is gradually reduced and finally vanishes.

Previous approaches for modeling Intrusion Detection System (IDS) have been on twofold: improving detection model(s) in terms of (i) feature selection of audit data through wrapper and filter methods and (ii) parameters optimization of detection model design, based on classification, clustering algorithms, etc. In this paper, we present three approaches to model IDS in the context of feature selection and parameters optimization: First, we present Fusion of Genetic Algorithm (GA) and Support Vector Machines (SVM) (FuGAS), which employs combinations of GA and SVM through genetic operation and it is capable of building an optimal detection model with only selected important features and optimal parameters value. Second, we present Correlation-based Hybrid Feature Selection (CoHyFS), which utilizes a filter method in conjunction of GA for feature selection in order to reduce long training time. Third, we present Simultaneous Intrinsic Model Identification (SIMI), which adopts Random Forest (RF) and shows better intrusion detection rates and feature selection results, along with no additional computational overheads. We show the experimental results and analysis of three approaches on KDD 1999 intrusion detection datasets.

Various advantages of cooperative peer-to-peer networks are strongly counterbalanced by the open nature of a distributed, serverless network. In such networks, it is relatively easy for an attacker to launch various attacks such as misrouting, corrupting, or dropping messages as a result of a successful identifier forgery. The impact of an identifier forgery is particularly severe because the whole network can be compromised by attacks such as Sybil or Eclipse. In this paper, we present an identifier authentication mechanism called random visitor, which uses one or more randomly selected peers as delegates of identity proof. Our scheme uses identity-based cryptography and identity ownership proof mechanisms collectively to create multiple, cryptographically protected indirect bindings between two peers, instantly when needed, through the delegates. Because of these bindings, an attacker cannot achieve an identifier forgery related attack against interacting peers without breaking the bindings. Therefore, our mechanism limits the possibility of identifier forgery attacks efficiently by disabling an attacker's ability to break the binding. The design rationale and framework details are presented. A security analysis shows that our scheme is strong enough against identifier related attacks and that the strength increases if there are many peers (more than several thousand) in the network.

Traditionally, it has been considered that the received signal to noise power ratio should be uniformly preserved to maximize system capacity for uncoded system with reliable feedback channel. However, once channel coding is employed as a building block, another power control scheme presents better performance. In this paper, we consider several power reallocation schemes for an effective use of limited power in a turbo coded system in lognormal shadowing channel. We show that the proposed power reallocation can reduce the decoding error probability by almost two orders of magnitude and provide a power gain of 0.87 dB at a target bit error rate of 10-4 over the equal power allocation among all code symbols. We also propose applying different power levels and cut-off thresholds on systematic and parity bits, and investigate the effect of channel estimation error.

Motion-compensated frame interpolation (MCFI) is widely used to smoothly display low frame rate video sequences by synthesizing and inserting new frames between existing frames. The temporal shift interpolation technique (TSIT) is popular for frame interpolation of video sequences that are encoded by a block-based video coding standard such as MPEG-4 or H.264/AVC. TSIT assumes the existence of a motion vector (MV) and may not result in high-quality interpolation for intra-mode blocks that do not have MVs. This paper proposes a new frame interpolation algorithm mainly designed for intra-mode blocks. In order to improve the accuracy of pixel interpolation, the new algorithm proposes sub-pixel interpolation and the reuse of MVs for their refinement. In addition, the new algorithm employs two different interpolation modes for inter-mode blocks and intra-mode blocks, respectively. The use of the two modes reduces ghost artifacts but potentially increases blocking effects between the blocks interpolated by different modes. To reduce blocking effects, the proposed algorithm searches the boundary of an object and interpolates all blocks in the object in the same mode. Simulation results show that the proposed algorithm improves PSNR by an average of 0.71 dB compared with the TSIT with MV refinement and also significantly improves the subjective quality of pictures by reducing ghost artifacts.

The delay time (tdT), power dissipation (PT) and circuit volume of a CMOS register array were minimized. Seven test circuits, each of which had a register array and a single clock tree that generated a pair of complement clock pulses, and a conventional register were fabricated using 90-nm CMOS technology. The register array was constructed with M delay flip-flops (FFs) and the clock tree, which consisted of 2 driver stages. Each driver stage had m inverters, each of which drove M/m FFs where M was fixed at 40 and m varied from 1 to 40. The minimum values of tdT and PT were 0.25 ns and 17.88 µW, respectively, and were both obtained when m was 10. These values were 71.4% and 70.4% of tdT and PT for the conventional register, for which m is 40, respectively. The number of inverters in the clock tree when m was 10 was 21 which was only 25.9% that for the conventional register. The measured results agreed well with SPICE-simulated results. Furthermore, for values of M from 20 to 320, both the minimum tdT and the minimum PT were obtained when m was approximately 1.5 times the square root of M.

This paper presents a design of an asynchronous peer-to-peer half-duplex/full-duplex-selectable data-transfer system on-chip interconnected. The data-transfer method between channels is based on a 1-phase signaling scheme realized by using multiple-valued current-mode (MVCM) circuits and encoding, which performs high-speed communication. A data transmission is selectable by adding a mode-detection circuit that observes data-transmission modes; full-duplex, half-duplex and standby modes. Especially, since current sources are completely cut off during the standby mode, the power dissipation can be greatly reduced. Moreover, both half-duplex and full-duplex communication can be realized by sharing a common circuit except a signal-level conversion circuit. The proposed interface is implemented using 0.18-µm CMOS, and its performance improvement is discussed in comparison with those of the other ordinary asynchronous methods.

We present a model checking approach to the rationale, implementation, and applications of a query language for location-based services. Such query mechanisms are necessary so that users, objects, and/or services can effectively benefit from the location-awareness of their surrounding environment. The underlying data model is founded on a symbolic model of space organized in a tree structure. Once extended to a semantic model for modal logic, we regard location query processing as a model checking problem, and thus define location queries as hybrid logic-based formulas. Our approach is unique to existing research because it explores the connection between location models and query processing in ubiquitous computing systems, relies on a sound theoretical basis, and provides modal logic-based query mechanisms for expressive searches over a decentralized data structure. A prototype implementation is also presented and will be discussed.