In this paper, we propose an unbounded model checking method for feature interaction verification for telecommunication systems. Unbounded model checking is a SAT-based verification method and has attracted recent attention as a powerful approach. The interpolation-based approach is one of the most promising unbounded model checking methods and has been proven to be effective for hardware verification. However, the application of unbounded model checking to asynchronous systems, such as telecommunication systems, has rarely been practiced. This is because, with the conventional encoding, the behavior of an asynchronous system can only be represented as a large propositional formula, thus resulting in large computational cost. To overcome this problem we propose to use a new scheme for encoding the behavior of the system and adapt the unbounded model checking algorithm to this encoding. By exploiting the concurrency of an asynchronous system, this encoding scheme allows a very concise formula to represent system's behavior. To demonstrate the effectiveness of our approach, we conduct experiments where 21 pairs of telecommunication services are verified using several methods including ours. The results show that our approach exhibits significant speed-up over unbounded model checking using the traditional encoding.

Security protocol provides communication security for the internet. One of the important features of it is authentication with key exchange. Its correctness is a requirement of the whole of the communication security. In this paper, we introduce three attack models realized as their attack scenarios, and provide an authentication-protocol checker for applying three attack-scenarios based on the models. We also utilize it to check two popular security protocols: Secure SHell (SSH) and Secure Socket Layer/Transport Layer Security (SSL/TLS).

In an embedded system where a single application or a class of applications is repeatedly executed on a processor, its cache configuration can be customized such that an optimal one is achieved. We can have an optimal cache configuration which minimizes overall memory access time by varying the three cache parameters: the number of sets, a line size, and an associativity. In this paper, we first propose two cache simulation algorithms: CRCB1 and CRCB2, based on Cache Inclusion Property. They realize exact cache simulation but decrease the number of cache hit/miss judgments dramatically. We further propose three more cache design space exploration algorithms: CRMF1, CRMF2, and CRMF3, based on our experimental observations. They can find an almost optimal cache configuration from the viewpoint of access time. By using our approach, the number of cache hit/miss judgments required for optimizing cache configurations is reduced to 1/10-1/50 compared to conventional approaches. As a result, our proposed approach totally runs an average of 3.2 times faster and a maximum of 5.3 times faster compared to the fastest approach proposed so far. Our proposed cache simulation approach achieves the world fastest cache design space exploration when optimizing total memory access time.

Frequency-domain equalization (FDE) based on the minimum mean square error (MMSE) criterion can provide better downlink bit error rate (BER) performance of direct sequence code division multiple access (DS-CDMA) than the conventional rake combining in a frequency-selective fading channel. FDE requires accurate channel estimation. In this paper, we propose a new 2-step maximum likelihood channel estimation (MLCE) for DS-CDMA with FDE in a very slow frequency-selective fading environment. The 1st step uses the conventional pilot-assisted MMSE-CE and the 2nd step carries out the MLCE using decision feedback from the 1st step. The BER performance improvement achieved by 2-step MLCE over pilot assisted MMSE-CE is confirmed by computer simulation.

We have introduced a new ultrasonic-based localization method that requires only one ultrasonic receiver to locate transmitters. In our previous reports [1],[2], we conducted several fundamental experiments, and proved the feasibility and accuracy of our system. However the performance in a more realistic environment has not yet been evaluated. In this paper, we have extended our localization system into a robot tracking system, and conducted experiments where the system tracked a moving robot. Localization was executed both by our proposed method and by the conventional TOA method. The experiment was repeated with different density of receivers. Thus we were able to compare the accuracy and the scalability between our proposed method and the conventional method. As a result 90-percentile of the position error was from 6.2 cm to 14.6 cm for the proposed method, from 4.0 cm to 6.1 cm for the conventional method. However our proposed method succeeded in calculating the position of the transmitter in 95% out of total attempts of localization with sparse receivers (4 receivers in about 5 m 5 m area), whereas the success rate was only 31% for the conventional method. From the result we concluded that although the proposed method is less accurate it can cover a wider area with sparse receivers than the conventional method. In addition to the dynamic tracking experiments, we also conducted some localization experiments where the robot stood still. This was because we wanted to investigate the reason why the localization accuracy degraded in the dynamic tracking. According to the result, the degradation of accuracy might be due to the systematic error in localization which is dependent on the geometric relationship between the transmitter and the receiver.

Secure sensor localization is a prerequisite for many sensor networks to retrieve trustworthy data. However, most of existing node positioning systems were studied in trust environment and are therefore vulnerable to malicious attacks. In this work, we develop a robust node positioning mechanism(ROPM) to protect localization techniques from position attacks. Instead of introducing countermeasures for every possible internal or external attack, our approach aims at making node positioning system attack-tolerant by removing malicious beacons. We defeat internal attackers and external attackers by applying different strategies, which not only achieves robustness to attacks but also dramatically reduces the computation overhead. Finally, we provide detailed theoretical analysis and simulations to evaluate the proposed technique.

We describe the applicability of photonic crystal fiber (PCF) with an enlarged effective area Aeff to a distributed Raman amplification (DRA) transmission. We investigate the DRA transmission performance numerically over a large Aeff PCF taking account of the signal-to-noise ratio (SNR) improvement RSNR in the S, C, and L bands. We show that an RSNR of 3 dB can be expected by utilizing DRA with a maximum pump power of 500 mW when the Aeff of the PCF is 230 µm2.

In this paper the time-domain analysis of two parallel traces is investigated. First, the telegrapher's equations for transmission line are applied to the parallel traces on printed circuit board (PCB), and are solved by using the mode decomposition technique. The time-domain solutions are then obtained by using the inverse Laplace transform. Although the Fourier-transform technique is also applicable for this problem, the solution is given numerically. Contrarily, the inverse Laplace transform successfully leads to an analytical expression for the transmission characteristics. The analytical expression is represented by series, which clearly explains the coupling mechanism. The analytical expression for the fundamental section of a meander delay line is investigated in detail. The analytical solution is validated by measurements, and the characteristics of the distortions in the output waveforms of meander delay lines due to the crosstalk are also investigated.

Continuous phase modulation (CPM) is a non-linear modulation technique whose power and bandwidth efficiency make it an attractive choice for mobile communication systems. Current research has focused on devising encoding rules for using CPM over multiple-input multiple-output (MIMO) systems in order to obtain the improved bit error rate (BER) and high data rates promised by MIMO technology. In this paper, optimal and suboptimal non-coherent receivers for a class of CPM signals called orthogonal space-time CPM (OST-CPM) are derived under a quasi-static fading channel assumption. The performance of these receivers is characterized and shown to achieve the same diversity order as that of the corresponding optimal coherent receiver.

Video summarization is defined as creating a video summary which includes only important scenes in the original video streams. In order to realize automatic video summarization, the significance of each scene needs to be determined. When targeted especially on broadcast sports videos, a play scene, which corresponds to a play, can be considered as a scene unit. The significance of every play scene can generally be determined based on the importance of the play in the game. Furthermore, the following two issues should be considered: 1) what is important depends on each user's preferences, and 2) the summaries should be tailored for media devices that each user has. Considering the above issues, this paper proposes a unified framework for user and device adaptation in summarizing broadcast sports videos. The proposed framework summarizes sports videos by selecting play scenes based on not only the importance of each play itself but also the users' preferences by using the metadata, which describes the semantic content of videos with keywords, and user profiles, which describe users' preference degrees for the keywords. The selected scenes are then presented in a proper way using various types of media such as video, image, or text according to device profiles which describe the device type. We experimentally verified the effectiveness of user adaptation by examining how the generated summaries are changed by different preference degrees and by comparing our results with/without using user profiles. The validity of device adaptation is also evaluated by conducting questionnaires using PCs and mobile phones as the media devices.

We have proposed a terahertz (THz) emitter utilizing two-dimensional plasmons (2DPs) in a super-grating dual-gate (SGG) high electron mobility transistor (HEMT). The plasmon under each grating gate has a unique feature that its resonant frequency is determined by the plasma-wave velocity over the gate length. Since the drain bias voltage causes a linear potential slope from the source to drain area, the sheet electron densities in periodically distributed 2DP cavities are dispersed. As a result, all the resonant frequencies are dispersed and undesirable spectral broadening occurs. A SGG structure can compensate for the sheet electron density distribution by modulating the grating dimension. The finite difference time domain simulation confirms its spectral narrowing effect. Within a wide detuning range for the gate and drain bias voltages giving a frequency shifting of 0.5 THz from an optimum condition, the SGG structure can preserve the spectral narrowing effect.

In this study, I have numerically investigated the temperature distribution of n-type Si Nano Wire MOS Transistor induced by the self-heating effect by using a 3-D device simulator. The dependencies of temperature distribution within the Si Nano Wire MOS Transistor on both its gate length and width of the Si nano wire were analyzed. First, it is shown that the peak temperature in Si Nano Wire MOS Transistor increases by 100 K with scaling the gate length from 54 nm to 14 nm in the case of a 50 nm width Si nano wire. Next, it is found that the increase of its peak temperature due to scaling the gate length can be suppressed by scaling the size of the Si nano wire, for the first time. The peak temperature suppresses by 160 K with scaling the Si nano wire width from 50 nm to 10 nm in the case of a gate length of 14 nm. Furthermore, the heat dissipation in the gate, drain, and source direction are analyzed, and the analytical theory of the suppression of the temperature inside Si Nano Wire MOSFET is proposed. This study shows very useful results for future Si Nano Wire MOS Transistor design for suppressing the self-heating effect.

We analyze the carrier dynamics in MOSFETs under low-voltage operation. For this purpose the displacement (charging/discharging) current, induced during switching operations is studied experimentally and theoretically for a 90 nm CMOS technology. It is found that the experimental transient characteristics can only be well reproduced in the circuit simulation of low voltage applications by considering the carrier-transit delay in the compact MOSFET model. Long carrier transit delay under the low voltage switching-on operation results in long duration of the displacement current flow. On the other hand, the switching-off characteristics are independent of the bias condition.

In this letter, we propose a simple but accurate calculation method, that is, an approximate closed-form equation of average bit error rate in DPSK/OFDM systems with post-detection diversity reception over both time- and frequency-selective Rayleigh fading channels. The validity of the proposed method is verified by the fact that BER performances given by the derived equation coincide with those by Monte Carlo simulation.

With the growth of the Internet, various types of services are rapidly expanding; such services include the World Wide Web (WWW), the File Transfer Protocol (FTP), and remote login. Consequently, managing authentication information, e.g., user ID/password pairs, keys, and certificates- is difficult for users, since the amount of required authentication information has been increased. To address this problem, researchers have developed a Single Sign-On (SSO) system that makes all the services available for a user via a one-time authentication: however, existing authentication systems cannot provide such SSO services for all kind of services on the Internet, even if the service provider deploys the SSO server. Further, existing systems also cannot provide the SSO service which does not make it conscious of a network domain to a user on secure network environment. Therefore, in this paper, we propose a new SSO system with a hardware token and a key management server to improve the safety, ubiquity, and adaptability of services. Further, we implement the proposed system and show its effectiveness through evaluation. Adding any functions for this system provides various conveniences to us. We also explore the ability to add functions to this system; for example, we add high trust connection functionality for a Web server and show its effectiveness.

Vector coding (VC) is a kind of eigen mode transmission scheme which is typically considered in MIMO systems. In VC systems, several code channels corresponding to the eigenvalues of the channel matrix are created. However, any code channels with low eigenvalues will cause a degradation in performance. In this paper, adaptive modulation and coding (AMC) for a VC system is proposed. In addition to AMC, the number of code channels is adaptively changed by code channel elimination. We show that the BER performance of VC is better than that of MMSE. Secondly, we also show the throughput performance of the proposed scheme is improved compared with the maximum throughput of each individual MCS.

In this paper, we introduce a unified framework based on a canonical decision diagram called Horner Expansion Diagram (HED) [1] for the purpose of equivalence checking of datapath oriented hardware designs in various design stages from an algorithmic description to the gate-level implementation. The HED is not only able to represent and manipulate algorithmic specifications in terms of polynomial expressions with modulo equivalence but also express bit level adder (BLA) description of gate-level implementations. Our HED can support modular arithmetic operations over integer rings of the form Z2n. The proposed techniques have successfully been applied to equivalence checking on industrial benchmarks. The experimental results on different applications have shown the significant advantages over existing bit-level and also word-level equivalence checking techniques.

Aiming at traditional neural networks non-uniformity correction (NUC) algorithm's disadvantages such as slow convergence, low correction precision and difficulty to meet the real-time engineering application requirements of infrared imaging system, an improved NUC algorithm for infrared focal plane arrays (IRFPA) based on neural network is proposed. The algorithm is based on linear response of detector, and in order to realize fast and synchronization convergence of correction parameters the each original image data is normalized to a value close to one. Experimental results show the method has the faster convergence speed and better vision effect than the traditional algorithms, and it is better applied in practical projects.

This paper discusses verification of the security against inference attacks on XML databases. First, a security definition called k-secrecy against inference attacks on XML databases is proposed. k-secrecy with an integer k > 1 (or k = ∞) means that attackers cannot narrow down the candidates for the value of the sensitive information to k - 1 (or finite), using the results of given authorized queries and schema information. Secondly, an XML query model such that verification can be performed straightforwardly according to the security definition is presented. The query model can represent practical queries which extract some nodes according to any of their neighboring nodes such as ancestors, descendants, and siblings. Thirdly, another refinement of the verification method is presented, which produces much smaller intermediate results if a schema contains no arbitrarily recursive element. The correctness of the refinement is proved, and the effect of the refinement in time and space efficiency has been confirmed by experiment.

Current collapse phenomenon is a well known obstacle in the AlGaN/GaN HEMTs. In order to improve the surface stability of HEMTs, we have investigated the SiN passivation film deposited by T-CVD, and we found that it improves both gate leakage current and current collapse phenomenon [1]. Moreover, we compared the T-CVD and PE-CVD passivation films, on high electric field DC and RF characteristics. We found that T-CVD SiN passivation film improves BVds-off by 30% because of the reduction of gate leakage current. It also improved ηd in the output power characteristics by load-pull measurement, which indicates the decrease of the current collapse phenomenon. Also we fabricated a multi-fingered 50 W-class AlGaN/GaN HEMT with T-CVD SiN passivation film and achieved 61.2% of high drain efficiency at frequency of 2.14 GHz, which was 3.6 points higher than that with PE-CVD SiN passivation film.