This paper presents a new technique to smooth speech feature vectors for text-independent speaker verification using an adaptive band-pass IIR filer. The filter is designed by considering the probability density of modulation-frequency components of an M-dimensional feature vector. Each dimension of the feature vector is processed and filtered separately. Initial filter parameters, low-cut-off and high-cut-off frequencies, are first determined by the global mean of the probability densities computed from all feature vectors of a given speech utterance. Then, the cut-off frequencies are adapted over time, i.e. every frame vector, in both low-frequency and high-frequency bands based also on the global mean and the standard deviation of feature vectors. The filtered feature vectors are used in a SVM-GMM Supervector speaker verification system. The NIST Speaker Recognition Evaluation 2006 (SRE06) core-test is used in evaluation. Experimental results show that the proposed technique clearly outperforms a baseline system using a conventional RelAtive SpecTrA (RASTA) filter.

The author developed a wideband precise I/Q modulator using GaAs pHEMT technology. In this technology, pHEMT has 0.22 µm metallurgical gate length and ft=51 GHz at Vds=5V. With the careful design of the wideband phase shifter, this IQ modulator achieved a large wideband frequency range of 250 MHz to 8 GHz and good EVM performance after calibration. For overall frequency range, low distortion performance is obtained, where third order intermodulation is less than -42 dBc. Also the ACPR at 2.2 GHz for W-CDMA application is less than -74 dBc.

This paper identifies a ripple effect problem (REP) that spreads interference to neighbors and proposes a novel channel localization mechanism to decrease the REP in a Wi-Fi system. The proposed mechanism has less blocking probability when compared to a random channel allocation mechanism and also has increased channel reusability. The proposed mechanism in simulation yields less channels BEm as the number of users and Tused increase.

At Eurocrypt'2006, Lu et al. proposed a pairing based verifiably encrypted signature scheme (the LOSSW-VES scheme) without random oracles. In this letter, we show that the LOSSW-VES scheme does not have opacity against rogue-key attacks.

This paper proposes a verification-aware design methodology that provides developers with a systematic and reliable approach to performing thread-pipelining parallelization on sequential programs. In contrast to traditional design flow, a behavior-model program is constructed before parallelizing as a bridge to help developers gradually leverage the technique of thread-pipelining parallelization. The proposed methodology integrates verification mechanisms into the design flow. To demonstrate the practicality of the proposed methodology, we applied it to the parallelization of a 3D depth map generator with thread pipelining. The parallel 3D depth map generator was further integrated into a 3D video playing system for evaluation of the verification overheads of the proposed methodology and the system performance. The results show the parallel system can achieve 33.72 fps in D1 resolution and 12.22 fps in HD720 resolution through a five-stage pipeline. When verifying the parallel program, the proposed verification approach keeps the performance degradation within 23% and 21.1% in D1 and HD720 resolutions, respectively.

In this letter, we adopt a new factor analysis of neighborhood-preserving embedding (NPE) for speaker verification. NPE aims at preserving the local neighborhood structure on the data and defines a low-dimensional speaker space called neighborhood-preserving embedding space. We compare the proposed method with the state-of-the-art total variability approach on the telephone-telephone core condition of the NIST 2008 Speaker Recognition Evaluation (SRE) dataset. The experimental results indicate that the proposed NPE method outperforms the total variability approach, providing up to 24% relative improvement.

The minimized assumption generation has been recognized as an important improvement of the assume-guarantee verification method in order to generate minimal assumptions. The generated minimal assumptions can be used to recheck the whole component-based software at a lower computational cost. The method is not only fitted to component-based software but also has a potential to solve the state space explosion problem in model checking. However, the computational cost for generating the minimal assumption is very high so the method is difficult to be applied in practice. This paper presents an optimization as a continuous work of the minimized assumption generation method in order to reduce the complexity of the method. The key idea of this method is to find a smaller assumption in a sub-tree of the search tree containing the candidate assumptions using the depth-limited search strategy. With this approach, the improved method can generate assumptions with a lower computational cost and consumption memory than the minimized method. The generated assumptions are also effective for rechecking the systems at much lower computational cost in the context of software evolution. An implemented tool supporting the improved method and experimental results are also presented and discussed.

A differential pair of convergent and divergent lenses with adjustable lens spacing (“differential lens”) was devised as a varifocal lens and was successfully integrated into an object-space telecentric lens to build a focus mechanism with constant magnification. This integration was done by placing the front principal point of the varifocal lens at the rear focal point of the telecentric lens within a practical tolerance of positioning. Although the constant-magnification focus mechanism is a parallel projection system, a system for perfect perspective projection imaging without shifting the projection center during focusing could be built simply by properly setting this focus mechanism between an image-taking lens with image-space telecentricity and an image sensor. The focus resolution experimentally obtained was 0.92 µm (σ) for the parallel projection system with a depth range of 1.0 mm and this was 0.25 mm (σ) for the perspective projection system with a range from 120 to 350 mm within a desktop space. A marginal image resolution of 100 lp/mm was obtained with optical distortion of less than 0.2% in the parallel projection system. The differential lens could work up to 55 Hz for a sinusoidal change in lens spacing with a peak-to-valley amplitude of 425 µm when a tiny divergent lens that was plano-concave was translated by a piezoelectric positioner. Therefore, images that were entirely in focus were generated at a frame rate of 30 Hz for an object moving at a speed of around 150 mm/s in depth within the desk top space. Thus, three-dimensional (3-D) imaging that provided 3-D resolution based on fast focusing was accomplished in both microscopic and macroscopic spaces.

This paper proposes a write resistance tracking circuit (WRTC) to improve the memory window of HfOx-based resistive memory. With a 50-ns single voltage pulse, the minimal resistance of the high resistance state in the 1-kb array of resistive switching elements can increase from 25 kΩ to 65 kΩ by using the proposed verify circuit. The WRTC uses the transition current detection method based on the feedback of the memory cell to control the write driver. The WRTC achieves distinct bistable resistance states, avoids the occurrence of over-RESET, and enhances the memory window of the RRAM cell.

This paper discusses verification of the security against inference attacks on XML databases in the presence of a functional dependency. So far, we have provided the verification method for k-secrecy, which is a metric for the security against inference attacks on databases. Intuitively, k-secrecy means that the number of candidates of sensitive data (i.e., the result of unauthorized query) of a given database instance cannot be narrowed down to k-1 by using available information such as authorized queries and their results. In this paper, we consider a functional dependency on database instances as one of the available information. Functional dependencies help attackers to reduce the number of the candidates for the sensitive information. The verification method we have provided cannot be naively extended to the k-secrecy problem with a functional dependency. The method requires that the candidate set can be captured by a tree automaton, but the candidate set when a functional dependency is considered cannot be always captured by any tree automaton. We show that the ∞-secrecy problem in the presence of a functional dependency is decidable when a given unauthorized query is represented by a deterministic topdown tree transducer, without explicitly computing the candidate set.

In this paper, a 60 nm-thick ferroelectric film of poly(vinylidene fluoride–trifluoroethylene) on a flexible substrate of aluminum foil was fabricated and characterized. Compared to pristine silicon wafer, Al-foil has very large root-mean-square (RMS) roughness, thus presenting challenges for the fabrication of flat and uniform electronic devices on such a rough substrate. In particular, RMS roughness affects the leakage current of dielectrics, the uniformity of devices, and the switching time in ferroelectrics. To avoid these kinds of problems, a new thin film fabrication method adopting a detach-and-transfer technique has been developed. Here, 'detach' means that the ferroelectric film is detached from a flat substrate (sacrificial substrate), and 'transfer' refers to the process of the detached film being moved onto the rough substrate (main substrate). To characterize the dielectric property of the transferred film, polarization and voltage relationships were measured, and the results showed that a hysteresis loop could be obtained with low leakage current.

In this paper, we discuss a fundamental theory of incremental verification for workflows. Incremental verification is a method to help multiple designers share and collaborate on huge workflows while maintaining their consistency. To this end, we introduce passbacks in workflows and their consistency property in the control flow perspective. passbacks indicate redoing of works. Workflows with passbacks are useful to naturally represent human works. To define the consistency property above, we define normality of workflows with passbacks and total correctness of normal workflows based on transition system-based semantics of normal workflows. We further extend workflows to sorted workflows and define their vertical division and composition. We also extend total correctness to normal sorted workflows, for the sake of incremental verification of a large-scale workflow with passbacks via vertical division and composition.

Initialize and weak-program erasing scheme is proposed to achieve high-performance and high-reliability Ferroelectric (Fe-) NAND flash solid-state drive (SSD). Bit-by-bit erase VTH control is achieved by the proposed erasing scheme and history effects in Fe-NAND is also suppressed. History effects change the future erase VTH shift characteristics by the past program voltage. The proposed erasing scheme decreases VTH shift variation due to history effects from ±40% to ±2% and the erase VTH distribution width is reduced from over 0.4 V to 0.045 V. As a result, the read and VPASS disturbance decrease by 42% and 37%, respectively. The proposed erasing scheme is immune to VTH variations and voltage stress. The proposed erasing scheme also suppresses the power and bandwidth degradation of SSD.

Strong designated verifier signature scheme (SDVS) allows a verifier to privately check the validity of a signature. Recently, Huang et al. first constructed an identity-based SDVS scheme (HYWS) in a stronger security model with non-interactive proof of knowledge, which holds the security properties of unforgeability, non-transferability, non-delegatability, and privacy of signer's identity. In this paper, we show that their scheme does not provide the claimed properties. Our analysis indicates that HYWS scheme neither resist on the designated verifier signature forgery nor provide simulation indistinguishability, which violates the security properties of unforgeability, non-delegatability and non-transferability.

Recently, numerous service discovery protocols have been introduced in the open literature. Unfortunately, many of them did not consider security issues, and for those that did, many security and privacy problems still remain. One important issue is to protect the privacy of a service provider while enabling an end-user to search an alternative service using multiple keywords. To deal with this issue, the existing protocols assumed that a directory server should be trusted or owned by each service provider. However, an adversary may compromise the directory server due to its openness property. In this paper, we suggest an efficient verification of service subscribers to resolve this issue and analyze its performance and security. Using this method, we propose an efficient and secure service discovery protocol protecting the privacy of a service provider while providing multiple keywords search to an end-user. Also, we provide performance and security analysis of our protocol.

A novel Template Updating system for fingerprint verification systems used in mobile applications is introduced in the paper. Based on the proposed method, the system performance is improved much more than the original one. Not only the FRR (False Reject Rate) but also the small overlap problem caused by the very narrow sensor on the mobile phone are solved. Based on the template updating system, templates are replaced with matched inputs towards a target structure which can expand the coverage of templates with large displacement and rotation. By using the test database, the system performance shows the FRR can be reduced by 79% in comparison with the one without template updating procedure. This system was adopted in practical mobile phones in the commercial market in 2009.

The Workflow Management Coalition, WfMC for short, has given a protocol for interorganizational workflows, interworkflows for short. In the protocol, an interworkflow is constructed by connecting two or more existing workflows; and there are three models to connect those workflows: chained, nested, and parallelsynchronized. Business continuity requires the interworkflow to preserve the behavior of the existing workflows. This requirement is called behavioral inheritance, which has three variations: protocol inheritance, projection inheritance, and life-cycle inheritance. Van der Aalst et al. have proposed workflow nets, WF-nets for short, and have shown that the behavioral inheritance problem is decidable but intractable. In this paper, we first show that all WF-nets of the chained model satisfy life-cycle inheritance, and all WF-nets of the nested model satisfy projection inheritance. Next we show that soundness is a necessary condition of projection inheritance for an acyclic extended free choice WF-net of the parallelsynchronized model. Then we prove that the necessary condition can be verified in polynomial time. Finally we show that the necessary condition is a sufficient condition if the WF-net is obtained by connecting state machine WF-nets.

This paper presents a verification and analysis tool set for embedded systems. Recently, the development scale of embedded systems has been increasing since they are used for mobile systems, automobile platforms, and various consumer systems with rich functionality. This has increased the amount of time and cost needed to develop them. Consequently, it is very important to develop tools to reduce development time and cost. This paper describes a tool set consisting of three tools to enhance the efficiency of embedded system design. The first tool is an integrated tool platform. The second is a remote debugging system. The third is a clock-accurate verification system based on a field-programmable gate array (FPGA) for custom embedded systems. This tool set promises to significantly reduce the time and cost needed to develop embedded systems.

Visibly pushdown automata (VPA), introduced by Alur and Madhusuan in 2004, is a subclass of pushdown automata whose stack behavior is completely determined by the input symbol according to a fixed partition of the input alphabet. Since it was introduced, VPA have been shown to be useful in various contexts, e.g., as specification formalism for verification and as an automaton model for processing XML streams. However, implementation of formal verification based on VPA framework is a challenge. In this paper, we propose on-the-fly algorithms to test universality and inclusion problems of this automata class. In particular, we first present a slight improvement on the upper bound for determinization of VPA. Next, in order to check universality of a nondeterministic VPA, we simultaneously determinize this VPA and apply the P-automata technique to compute a set of reachable configurations of the target determinized VPA. When a rejecting configuration is found, the checking process stops and reports that the original VPA is not universal. Otherwise, if all configurations are accepting, the original VPA is universal. Furthermore, to strengthen the algorithm, we define a partial ordering over transitions of P-automaton, and only minimal transitions are used to incrementally generate the P-automaton. The purpose of this process is to keep the determinization step implicitly for generating reachable configurations as minimum as possible. This improvement helps to reduce not only the size of the P-automaton but also the complexity of the determinization phase. We implement the proposed algorithms in a prototype tool, named VPAchecker. Finally, we conduct experiments on randomly generated VPA. The experimental results show that the proposed method outperforms the standard one by several orders of magnitude.

In processing stream data, time is one of the most significant facts not only because the size of data is dramatically increased but because the characteristics of data is varying over time. To learn stream data evolving over time effectively, it is required to detect the drift of concept. We present a window adaptation function on domain value (WAV) to determine the size of windowed batch for learning algorithms of stream data and a method to detect the change of data characteristics with a criterion function utilizing correlation. When applying our adaptation function to a clustering task on a multi-stream data model, the result of learning synopsis of windowed batch determined by it shows its effectiveness. Our criterion function with correlation information of value distribution over time can be the reasonable threshold to detect the change between windowed batches.