This paper proposes a framework for modular verification of evolving component-based software. This framework includes two stages: modular conformance testing for updating inaccurate models of the evolved components and modular verification for evolving component-based software. When a component is evolved after adapting some refinements, the proposed framework focuses on this component and its model in order to update the model and recheck the whole evolved system. The framework also reuses the previous verification results and the previous models of the evolved components to reduce the number of steps required in the model update and modular verification processes. An implementation and some experimental results are presented.

In PKC 2004, Choi et al. proposed an ID-based authenticated group key agreement (AGKA) protocol using bilinear pairings. Unfortunately, their protocol suffered from an impersonation attack and an insider colluding attack. In 2008, Choi et al. presented an improvement to resist insider attacks. In their modified protocol, they used an ID-based signature scheme on transcripts for binding them in a session to prevent replay of transcripts. In particular, they smartly used the batch verification technique to reduce the computational cost. In this paper, we first show that Choi et al.'s modified AGKA protocol still suffers from an insider colluding attack. Then, we prove that the batch verification of the adopted ID-based signature scheme in their modified protocol suffers from a forgery attack.

The GMM-UBM framework has been proved to be one of the most effective approaches to the automatic speaker verification (ASV) task in recent years. In this letter, we first propose an approximate decision function of traditional GMM-UBM, from which it is shown that the contribution to classification of each Gaussian component is equally important. However, research in speaker perception shows that a different speech sound unit defined by Gaussian component makes a different contribution to speaker verification. This motivates us to emphasize some sound units which have discriminability between speakers while de-emphasize the speech sound units which contain little information for speaker verification. Experiments on 2006 NIST SRE core task show that the proposed approach outperforms traditional GMM-UBM approach in classification accuracy.

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.

Equivalence checking is one of the most important issues in VLSI design to guarantee that bugs do not enter designs during optimization steps or synthesis steps. In this paper, we propose a new word-level equivalence checking method between two models before and after high-level synthesis or behavioral optimization. Our method converts two given designs into RTL models which have same datapaths so that behaviors by identical control signals become the same in the two designs. Also, functional units become common to the two designs. Then word-level equivalence checking techniques can be applied in bit-level accuracy. In addition, we propose a rule-based equivalence checking method which can verify designs which have complicated control structures faster than existing symbolic simulation based methods. Experimental results with realistic examples show that our method can verify such designs in practical periods.

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.

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.

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.

Probabilistic model checking is an emerging verification technology for probabilistic analysis. Its use has been started not only in computer science but also in interdisciplinary fields. In this paper, we show that probabilistic model checking allows one to analyze the magnetic behaviors of the one-dimensional Ising model, which describes physical phenomena of magnets. The Ising model consists of elementary objects called spins and its dynamics is often represented as the Metropolis method. To analyze the Ising model with probabilistic model checking, we build Discrete Time Markov Chain (DTMC) models that represent the behavior of the Ising model. Two representative physical quantities, i.e., energy and magnetization, are focused on. To assess these quantities using model checking, we devise formulas in Probabilistic real time Computation Tree Logic (PCTL) that represent the quantities. To demonstrate the feasibility of the proposed approach, we show the results of an experiment using the PRISM model checker.

Software model checking is typically applied to components of large systems. The assumption generation is the problem of finding the least restrictive environment in which the components satisfy a given safety property. There is an algorithm to compute the environment for properties given as a regular language. In this paper, we propose a general scheme for computing the assumption even for non-regular properties, and show the uniqueness of the least restrictive assumption for any class of languages. In general, dealing with non-regular languages may fall into undecidability of problems. We also show a method to compute assumptions based on visibly pushdown automata and their finite-state abstractions.

We propose an authentication scheme in which users can be authenticated anonymously so long as times that they are authenticated is within an allowable number. The proposed scheme has two features: 1) no one, not even an authority, can identify users who have been authenticated within the allowable number, 2) anyone can trace, without help from the authority, dishonest users who have been authenticated beyond the allowable number by using the records of these authentications. Our scheme can be applied to e-voting, e-cash, electronic coupons, and trial browsing of content. In these applications, our scheme, unlike the previous one, conceals users' participation from protocols and guarantees that they will remain anonymous to everyone.

In multi-FPGA prototyping systems for circuit verification, serialized time-multiplexed I/O technique is used because of the limited number of I/O pins of an FPGA. The verification time depends on a selection of inter-FPGA signals to be time-multiplexed. In this paper, we propose a method that minimizes the verification time of multi-FPGA systems by finding an optimal selection of inter-FPGA signals to be time-multiplexed. In the experiments, it is shown that the estimated verification time is improved 38.2% on average compared with conventional methods.

Recently much attention has been paid to quantum circuit design to prepare for the future "quantum computation era." Like the conventional logic synthesis, it should be important to verify and analyze the functionalities of generated quantum circuits. For that purpose, we propose an efficient verification method for quantum circuits under a practical restriction. Thanks to the restriction, we can introduce an efficient verification scheme based on decision diagrams called Decision Diagrams for Matrix Functions (DDMFs). Then, we show analytically the advantages of our approach based on DDMFs over the previous verification techniques. In order to introduce DDMFs, we also introduce new concepts, quantum functions and matrix functions, which may also be interesting and useful on their own for designing quantum circuits.

Functional and formal verification are important methodologies for complex mixed-signal design validation. However the industry is still verifying such systems by pure simulation. This process lacks on error localization and formal verifications methods. This is the existing verification gap between the analog and digital blocks within a mixed-signal system. Our approach improves the verification process by creating temporal properties named mixed-signal assertions which are described by a combination of digital assertions and analog properties. The proposed method is a new assertion-based verification flow for designing mixed-signal circuits. The effectiveness of the approach is demonstrated on a Σ/Δ-converter.

This paper suggests word voiceprint models to verify the recognition results obtained from a speech recognition system. Word voiceprint models have word-dependent information based on the distributions of phone-level log-likelihood ratio and duration. Thus, we can obtain a more reliable confidence score for a recognized word by using its word voiceprint models that represent the more proper characteristics of utterance verification for the word. Additionally, when obtaining a log-likelihood ratio-based word voiceprint score, this paper proposes a new log-scale normalization function using the distribution of the phone-level log-likelihood ratio, instead of the sigmoid function widely used in obtaining a phone-level log-likelihood ratio. This function plays a role of emphasizing a mis-recognized phone in a word. This individual information of a word is used to help achieve a more discriminative score against out-of-vocabulary words. The proposed method requires additional memory, but it shows that the relative reduction in equal error rate is 16.9% compared to the baseline system using simple phone log-likelihood ratios.

This paper presents a text-independent speaker verification method using Gaussian mixture models (GMMs), where only utterances of enrolled speakers are required. Artificial cohorts are used instead of those from speaker databases, and GMMs for artificial cohorts are generated by changing model parameters of the GMM for a claimed speaker. Equal error rates by the proposed method are about 60% less than those by a conventional method which also uses only utterances of enrolled speakers.

This paper presents a formal approach to verify arithmetic circuits using symbolic computer algebra. Our method describes arithmetic circuits directly with high-level mathematical objects based on weighted number systems and arithmetic formulae. Such circuit description can be effectively verified by polynomial reduction techniques using Grobner Bases. In this paper, we describe how the symbolic computer algebra can be used to describe and verify arithmetic circuits. The advantageous effects of the proposed approach are demonstrated through experimental verification of some arithmetic circuits such as multiply-accumulator and FIR filter. The result shows that the proposed approach has a definite possibility of verifying practical arithmetic circuits.

Many Internet services and protocols should guarantee anonymity; for example, an electronic voting system should guarantee to prevent the disclosure of who voted for which candidate. To prove trace anonymity, which is an extension of the formulation of anonymity by Schneider and Sidiropoulos, this paper presents an inductive method based on backward anonymous simulations. We show that the existence of an image-finite backward anonymous simulation implies trace anonymity. We also demonstrate the anonymity verification of an e-voting protocol (the FOO protocol) with our backward anonymous simulation technique. When proving the trace anonymity, this paper employs a computer-assisted verification tool based on a theorem prover.

In on-line signature verification, complexity of signature shape can influence the value of the optimal threshold for individual signatures. Writer-dependent threshold selection has been proposed but it requires forgery data. It is not easy to collect such forgery data in practical applications. Therefore, some threshold equalization method using only genuine data is needed. In this letter, we propose three different threshold equalization methods based on the complexity of signature. Their effectiveness is confirmed in experiments using a multi-matcher DWT on-line signature verification system.

This paper proposes an image authentication method that detects tamper and localizes tampered areas efficiently. The efficiency of the proposed method is summarized as the following three points. 1) This method offers coarse-to-fine tamper localization by hierarchical data hiding so that further tamper detection is suppressed for blocks labeled as genuine in the uppper layer. 2) Since the image feature description in the top layer is hidden over an image, the proposed method enciphers the data in the top layer rather than enciphers all data in all layers. 3) The proposed method is based on the reversible data hiding scheme that does not use highly-costed compression technique. These three points makes the proposed method superior to the conventional methods using compression techniques and methods using multi-tiered data hiding that requires integrity verification in many blocks even the image is genuine. Simulation results show the effectiveness of the proposed method.