In this paper we report on experiences gained and lessons learned by the use of the Timed OTS/CafeOBJ method in the formal verification of TESLA source authentication protocol. These experiences can be a useful guide for the users of the OTS/CafeOBJ, especially when dealing with such complex systems and protocols.

There have been many researches about construction and application of ontology in reality, notably the usage of ontology to support requirements engineering. The effect of ontology-based requirements engineering depends on quality of ontology. With the increasing size of ontology, it is difficult to verify the correctness of information stored in ontology. This paper will propose a method of using rules for verification the correctness of requirements ontology. We provide a rule description language to specify properties that requirements ontology should satisfy. Then, by checking whether the rules are consistent with requirements ontology, we verify the correctness of the ontology. We have developed a verification tool to support the method and evaluated the tool through experiments.

This paper introduces an ontology-based method for checking requirements specification. Requirements ontology is a knowledge structure that contains functional requirements (FR), attributes of FR and relations among FR. Requirements specification is compared with functional nodes in the requirements ontology, then rules are used to find errors in requirements. On the basis of the results, requirements team can ask questions to customers and correctly and efficiently revise requirements. To support this method, an ontology-based checking tool for verification of requirements has been developed. Finally, the requirements checking method is evaluated through an experiment.

With the development of global navigation satellite systems (GNSS), the interference among global navigation satellite systems, known as the radio frequency compatibility problem, has become a matter of great concern to system providers and user communities. The acceptable compatibility threshold should be determined in the radio frequency compatibility assessment process. However, there is no common standard for the acceptable threshold in the radio frequency compatibility assessment. This paper firstly introduces the comprehensive radio frequency compatibility methodology combining the spectral separation coefficient (SSC) and code tracking spectral sensitivity coefficient (CT_SSC). Then, a method for determination of the acceptable compatibility threshold is proposed. The proposed method considers the receiver processing phase including acquisition, code and carrier tracking and data demodulation. Simulations accounting for the interference effects are carried out at each time step and every place on earth. The simulations mainly consider the signals of GPS, Galileo and BeiDou Navigation Satellite System (BDS) in the L1 band. Results show that all of the sole systems are compatible with other GNSS systems with respect to a special receiver configuration used in the simulations.

The complicated indoor environment such as obstacles causes the non-line of sight (NLOS) environment. In this paper, we propose a voting matrix based residual weighting (VM-Rwgh) algorithm to mitigate NLOS errors in indoor localization system. The voting matrix is employed to provide initial localization results. The residual weighting is used to improve the localization accuracy. The VM-Rwgh algorithm can overcome the effects of NLOS errors, even when more than half of the measurements contain NLOS errors. Simulation results show that the VM-Rwgh algorithm provides higher location accuracy with relatively lower computational complexity in comparison with other methods.

An energy-efficient ΔΣ modulator using a novel switched-capacitor-based integrator has been investigated. The proposed dynamic integrator uses a common-source configuration, where a MOSFET turns off after the charge redistribution is completed. Thus, only the subthreshold current flows through the integrator, resulting in high energy efficiency. A constant threshold voltage works as the virtual ground in conventional opamp-based integrators. The performance has been estimated for a 2nd-order ΔΣ modulator by transistor-level circuit simulation assuming a 0.18-µm standard CMOS technology. An FOM of 29fJ/conv-step was obtained with a peak SNDR of 82.6dB for a bandwidth and a sampling frequency of 20kHz and 5MHz, respectively.

In this letter, we address monaural source separation based on supervised nonnegative matrix factorization (SNMF) and propose a new penalized SNMF. Conventional SNMF often degrades the separation performance owing to the basis-sharing problem. Our penalized SNMF forces nontarget bases to become different from the target bases, which increases the separated sound quality.

In this letter, we present a radix-R regular interconnection pattern family of factorizations for the WHT-FFT with identical stage-to-stage interconnection pattern in a unified form, where R is any power of 2. This family of algorithms has identical sparse matrix factorization in each stage and can be implemented in a merged butterfly structure, which conduce to regular and efficient memory managing scalable to high radices. And in each stage, the butterflies with same twiddle factor set are aggregated together, which can reduce the twiddle factor evaluations or accesses to the lookup table. The kinds of factorization can also be extended to FFT, WHT and SCHT with identical stage-to-stage interconnection pattern.

This letter presents a novel method based on sparsity, to solve the problem of deinterleaving pulse trains. The proposed method models the problem of deinterleaving pulse trains as an underdetermined system of linear equations. After determining the mixing matrix, we find sparsest solution of an underdetermined system of linear equations using basis pursuit denoising. This method is superior to previous ones in a number of aspects. First, spurious and missing pulses would not cause any performance reduction in the algorithm. Second, the algorithm works well despite the type of pulse repetition interval modulation that is used. Third, the proposed method is able to separate similar sources.

In this paper we apply angle recoding to the CORDIC-based processing elements in a scalable architecture for complex matrix inversion. We extend the processing elements from the scalable real matrix inversion architecture to the complex domain and obtain the novel scalable complex matrix inversion architecture, which can significantly reduce computational complexity. We rearrange the CORDIC elements to make one half of the processing elements simple and compact. For the other half of the processing elements, the efficient use of angler recoding reduces the number of microrotation steps of the CORDIC elements to 3/4. Consequently, only 3 CORDIC elements are required for the processing elements with full utilization.

Turbo mode, which accelerates many applications without major change of existing systems, is widely used in commercial processors. Since time duration or powerfulness of turbo mode depends on peak temperature of a processor chip, reducing the peak temperature can reinforce turbo mode. This paper presents that adding small amount of hardware allows microprocessors to reduce the peak temperature drastically and then to reinforce turbo mode successfully. Our approach is to find out a few small units that become heat sources in a processor and to appropriately duplicate them for reduction of their power density. By duplicating the limited units and using the copies evenly, the processor can show significant performance improvement while achieving area-efficiency. The experimental result shows that the proposed method achieves up to 14.5% of performance improvement in exchange for 2.8% of area increase.

The millimeter-wave band suffers strong attenuation due to rain. While calculating the link budget for a wireless system using this frequency band, the behavior of rain, attenuation due to rain, and the amount of degradation must be accurately understood. This paper presents an evaluation of the influence of rain and its attenuation on link performance in a Tokyo Institute of Technology (Tokyo Tech) millimeter-wave model mesh network. Conventional statistical analyses including cumulative rain rate distribution and specific rain attenuation constants are performed on data collected from 2009 onwards. The unique effects arising due to the highly localized behaviors of strong rainfalls have become clear and are characterized in terms of variograms rather than correlation coefficients. Spatial separation even in the small network here with links of less than 1 km provides effective diversity branches for better availability performance.

The stochastic behavior of inter-core crosstalk in multi-core fiber is discussed based on a theoretical model validated by measurements, and the effect of the crosstalk on the Q-factor in transmission systems, using multi-core fiber is investigated theoretically. The measurements show that the crosstalk rapidly changes with wavelength, and gradually changes with time, in obedience to the Gaussian distribution in I-Q planes. Therefore, the behavior of the crosstalk as a noise may depend on the bandwidth of the signal light. If the bandwidth is adequately broad, the crosstalk may behave as a virtual additive white Gaussian noise on I-Q planes, and the Q-penalty at the Q-factor of 9.8dB is less than 1dB when the statistical mean of the crosstalk from other cores is less than -16.7dB for PDM-QPSK, -23.7dB for PDM-16QAM, and -29.9dB for PDM-64QAM. If the bandwidth is adequately narrow, the crosstalk may behave as virtually static coupling that changes very gradually with time and heavily depends on the wavelength. To cope with a static crosstalk much higher than its statistical mean, a margin of several decibels from the mean crosstalk may be necessary for suppressing Q-penalty in the case of adequately narrow bandwidth.

Collaborative business has been increasingly developing with the environment of globalization and advanced information technologies. In a collaboration environment with multiple organizations, participants from different organizations always have different views about modeling the overall business process due to different knowledge and cultural backgrounds. Moreover, flexible support, privacy preservation and process reuse are important issues that should be considered in business process management across organizational boundaries. This paper presents a novel approach of modeling interorganizational business process for collaboration. Our approach allows for modeling loosely coupled interorganizational business process considering different views of organizations. In the proposed model, organizations have their own local process views of modeling business process instead of sharing pre-defined global processes. During process cooperation, local process of an organization can be invisible to other organizations. Further, we propose the coordination mechanisms for different local process views to detect incompatibilities among organizations. We illustrate our proposed approach by a case study of interorganizational software development collaboration.

In the process of production design, engineers usually find it is difficult to seek and reuse others' empirical knowledge which is in the forms of lesson-learned documents. This study proposed a novel approach, which uses a semantic-based topic knowledge map system (STKMS) to support timely and precisely lesson-learned documents finding and reusing. The architecture of STKMS is designed, which has five major functional modules: lesson-learned documents pre-processing, topic extraction, topic relation computation, topic weights computation, and topic knowledge map generation modules. Then STKMS implementation is briefly introduced. We have conducted two sets of experiments to evaluate quality of knowledge map and the performance of utilizing STKMS in outfitting design of a ship-building company. The first experiment shows that knowledge maps generated by STKMS are accepted by domain experts from the evaluation since precision and recall are high. The second experiment shows that STKMS-based group outperforms browse-based group in both learning score and satisfaction level, which are two measurements of performance of utilizing STKMS. The promising results confirm the feasibility of STKMS in helping engineers to find needed lesson-learned documents and reuse related knowledge easily and precisely.

To realize usability in software, GUI (Graphical User Interface) layouts must be consistent because consistency allows end users to operate software based on previous experiences. Often consistency can be achieved by user interface guidelines, which realize consistency in a software package as well as between various software packages within a platform. Because end users have different experiences and perceptions, GUIs based on guidelines are not always usable for end users. Thus, it is necessary to realize consistency without guidelines. Herein we propose a method to realize consistent GUIs where existing software packages are surveyed and common patterns for window layouts, which we call layout rules, are specified. Our method uses these layout rules to arrange the windows of GUIs. Concretely, source programs of developed GUIs are analyzed to identify the layout rules, and then these rules are used to extract parameters to generate source programs of undeveloped GUIs. To evaluate our method, we applied it to existing GUIs in software packages to extract the layout rules from several windows and to generate other windows. The evaluation confirms that our method easily realizes layout consistency.

A workflow may be extended to adapt to market growth, legal reform, and so on. The extended workflow must be logically correct, and inherit the behavior of the existing workflow. Even if the extended workflow inherits the behavior, it may be not logically correct. Can we modify it so that it satisfies not only behavioral inheritance but also logical correctness? This is named behavioral inheritance preserving soundizability problem. There are two kinds of behavioral inheritance: protocol inheritance and projection inheritance. In this paper, we tackled protocol inheritance preserving soundizability problem using a subclass of Petri nets called workflow nets. Limiting our analysis to acyclic free choice workflow nets, we formalized the problem. And we gave a necessary and sufficient condition on the problem, which is the existence of a key structure of free choice workflow nets called TP-handle. Based on this condition, we also constructed a polynomial time procedure to solve the problem.

This letter presents a new entropy measure for electroencephalograms (EEGs), which reflects the underlying dynamics of EEG over multiple time scales. The motivation behind this study is that neurological signals such as EEG possess distinct dynamics over different spectral modes. To deal with the nonlinear and nonstationary nature of EEG, the recently developed empirical mode decomposition (EMD) is incorporated, allowing an EEG to be decomposed into its inherent spectral components, referred to as intrinsic mode functions (IMFs). By calculating Shannon entropy of IMFs in a time-dependent manner and summing them over adaptive multiple scales, the result is an adaptive subscale entropy measure of EEG. Simulation and experimental results show that the proposed entropy properly reveals the dynamical changes over multiple scales.

In this paper, we propose a fully parallel Turbo decoder for Software-Defined Radio (SDR) on the Graphics Processing Unit (GPU) platform. Soft Output Viterbi algorithm (SOVA) is chosen for its low complexity and high throughput. The parallelism of SOVA is fully analyzed and the whole codeword is divided into multiple sub-codewords, where the turbo-pass decoding procedures are performed in parallel by independent sub-decoders. In each sub-decoder, an efficient initialization method is exploited to assure the bit error ratio (BER) performance. The sub-decoders are mapped to numerous blocks on the GPU. Several optimization methods are employed to enhance the throughput, such as the memory optimization, codeword packing scheme, and asynchronous data transfer. The experiment shows that our decoder has BER performance close to Max-Log-MAP and the peak throughput is 127.84Mbps, which is about two orders of magnitude faster than that of central processing unit (CPU) implementation, which is comparable to application-specific integrated circuit (ASIC) solutions. The presented decoder can achieve higher throughput than that of the existing fastest GPU-based implementation.

In this paper, a one-class Naïve Bayesian classifier (One-NB) for detecting toll frauds in a VoIP service is proposed. Since toll frauds occur irregularly and their patterns are too diverse to be generalized as one class, conventional binary-class classification is not effective for toll fraud detection. In addition, conventional novelty detection algorithms have struggled with optimizing their parameters to achieve a stable detection performance. In order to resolve the above limitations, the original Naïve Bayesian classifier is modified to handle the novelty detection problem. In addition, a genetic algorithm (GA) is employed to increase efficiency by selecting significant variables. In order to verify the performance of One-NB, comparative experiments using five well-known novelty detectors and three binary classifiers are conducted over real call data records (CDRs) provided by a Korean VoIP service company. The experimental results show that One-NB detects toll frauds more accurately than other novelty detectors and binary classifiers when the toll frauds rates are relatively low. In addition, The performance of One-NB is found to be more stable than the benchmark methods since no parameter optimization is required for One-NB.