Most of current codesign tools or methodologies only support validation in the form of cosimulation and testing of design alternatives. The results of hardware-software codesign of a distributed system are often not verified, because they are not easily verifiable. In this paper, we propose a new formal coverification approach based on linear hybrid automata, and an algorithm for automatically converting codesign results to the linear hybrid automata framework. Our coverification approach allows automatic verification of real-time constraints such as hard deadlines. Another advantage is that the proposed approach is suitable for verifying distributed systems with arbitrary communication patterns and system architecture. The feasibility of our approach is demonstrated through several application examples. The proposed approach has also been successfully used in verifying deadline violations when there are inter-task communications between tasks with different period lengths.

This paper presents a universally verifiable Mix-net where the amount of work done by a verifier is independent of the number of mix-servers. Furthermore, the computational task of each mix-server is constant with regard to the number of mix-servers except for some negligible tasks like computing hash function when no disruption occurs. The scheme also provides robustness.

This paper proposes a model checking method for microcomputer programs. To deal with the state explosion problem, we adopt a compositional verification approach. Based on the proposed method, a microcomputer program for a real-life air-conditioner is verified. The program is large enough to cause state explosion. Among fourteen typical properties of the program, five properties are successfully verified by our method.

This paper proposes a method of automatically eliciting knowledge which is used to detect feature interactions in telecommunication services. With conventional methods, the knowledge is provided manually. With the proposed method, the knowledge is automatically elicited as service constraints. In telecommunication systems, when a new service is added, new state transitions are created. In case of new service, the new state should be reached in the state transitions. On the other hand, some states of existing services should not be reached. These constraints can be considered as knowledge for detecting feature interactions. This paper also proposes a scenario for detecting feature interactions using elicited knowledge. This scenario was confirmed as effective.

This paper presents a non-interactive and optimally resilient distributed multiplication scheme. By non-interactive we mean that the players need to use outgoing communication channels only once without the need to synchronize with the other players as long as no disruption occurs. Our protocol withstands corrupt players up to less than the half of the players, so it provides optimal resiliency. Furthermore, the shared secrets are secure even against infinitely powerful adversaries. The security is proven under the intractability assumption of the discrete logarithm problem. Those properties are achieved by using an information theoretically secure non-interactive verifiable secret sharing as a kind of non-interactive proof system between a single prover and distributed verifiers. Compared to a former interactive solution in the same setting, the cost is an increase in local computation and communication complexity that is determined by the factor of the threshold used in the verifiable secret sharing.

There are two approaches for formal verification of sequential designs or finite state machines: language containment checking and symbolic model checking. To verify designs of practical size, in these two approaches, designs are represented symbolically, in practice, by ordered binary decision diagrams. In the conventional algorithm for language containment checking, finite automata given as specifications are also represented symbolically. This paper proposes a new method, called partially explicit method for checking language containment. By representing states of finite automata given as specifications explicitly, this method can remove redundant computations, and as a result, provide better performance than the conventional method which uses the product machines of designs and specifications. The experimental results show that this approach is effective in checking language containment symbolically.

We present a symbolic language emptiness check algorithm based on forward state traversal. A verification property is given by a set of error traces written in ω-regular expression and is manipulated explicitly as a non-deterministic state transition graph. State space of the design model is implicitly traversed along the explicit graph. This method has a large amount of flexibility for controlling state traversal on the property space. It should become a good framework of incremental or approximate verification of ω-regular properties.

The minimum mean-squared error (MMSE) linear detector has been proposed to successfully suppress the multiple access interference and mitigate the near-far problem in direct-sequence code-division multiple access communication systems. In the presence of unknown or time-varying channel parameters, the MMSE linear detector can be implemented by the blind Griffiths' algorithm, which uses the desired signal vector instead of a training sequence of symbols for initial adaptation. In this paper, a variable step-size (VSS) Griffiths' algorithm is proposed for accelerating the convergence speed, especially in the presence of strong interference. Numerical results show that the convergence properties of the VSS Griffiths' algorithm are robust against the wide eigenvalue-spread problem of the correlation matrix associated with the received signal vector compared to the Griffiths' algorithm using a fixed step-size.

This paper presents an improved method of speaker verification using the sequential probability ratio test (SPRT), which can treat the correlation between successive feature vectors. The hidden Markov model with the mean field approximation enables us to consider the correlation in the SPRT, i. e. , using the mean field of previous state, probability computation can be carried out as if input samples were independent each other.

CTL (Computation Tree Logic) model checking is a formal method for design verification that checks whether the behavior of the verified system is contained in that of the requirements specification. If this check doesn't pass, the CTL model checker generates a subset of fair states which belongs to the system but not to the specification. In this letter, we present an incremental method which successively modifies the latest verification result each time the design is modified. Our incremental algorithm allows the designer to make changes in terms of addition or subtraction of fair CTL formulas, or fairness constraints on acceptable behavior from the problem statement. Then, these changes are adopted to update the set of fair states computed earlier. Our incremental algorithm is shown to be better than the current non-incremental techniques for CTL model checking. Furthermore, a conclusion supported by the experimental results is presented herein.

In this paper, near real time digital radiography system was implemented for the automatic verification of local errors between simulation plan and radiation therapy. Portal image could be acquired through video camera, image board and PC after therapy radiation was converted into light by a metal/fluorescent screen. Considering the divergence according to the distance between the source and the plate, we made a 340 340 12 cm3 basis point plate on which five rods of 4 cm height and 8 mm diameter lead (Pb) were built to display reference points on the simulator and the portal image. We converted the portal image into the binary image using the optimal threshold value which was gotten through the histogram analysis of the acquired portal image using the basis point plate. we got the location information of the iso-center and basis points from the binary image, and removed the systematic errors which were from the differences between the simulation plan and the portal image. Field size which was measured automatically by optimal threshold portal image, was verified with simulation plan. Anatomic errors were automatically detected and verified with the normalized simulation and the portal image by pattern matching method after irradiating a part of the radiation. Therapy efficiency was improved and radiation side effects were reduced by these techniques, so exact radiation treatment are expected.

The full-band Monte Carlo technique is currently the most accurate device simulation method, but its usefulness is limited because it is very CPU intensive. This work describes efficient algorithms in detail, which raise the efficiency of the full-band Monte Carlo method to a level where it becomes applicable in the device design process beyond exemplary simulations. The k-space is discretized with a nonuniform tetrahedral grid, which minimizes the discretization error of the linear energy interpolation and memory requirements. A consistent discretization of the inverse mass tensor is utilized to formulate efficient transport parameter estimators. Particle scattering is modeled in such a way that a very fast rejection technique can be used for the generation of the final state eliminating the main cause of the inefficiency of full-band Monte Carlo simulations. The developed full-band Monte Carlo simulator is highly efficient. For example, in conjunction with the nonself-consistent simulation technique CPU times of a few CPU minutes per bias point are achieved for substrate current calculations. Self-consistent calculations of the drain current of a 60nm-NMOSFET take about a few CPU hours demonstrating the feasibility of full-band Monte Carlo simulations.

The Scalable-Delay-Insensitive (SDI) model is proposed for high-performance asynchronous system design. In this paper, we focus on checking whether a circuit under SDI model satisfies some untimed properties, and formally show that checking these properties in the SDI model can be reduced to checking the same properties in the bounded delay model. This result suggests that the existing verification algorithms for the bounded delay model can be used for the verification of SDI circuits, which significantly helps the designers of SDI circuits.

This paper describes an algorithm and its prototype system--VeriProc/1. 1--which can prove the correctness of pipelined and superscalar processor controls automatically without a pipeline invariant, human interaction, or additional information. This algorithm is based on behavior-covering and partial unfolding. No timing relations such as an abstract function or β-relation is required. The only information required is to specify the location of the selectors in the design. Partial unfolding makes it possible to derive superscalar specifications from conventional specifications. Correctness proof of the partial unfolding is given. The prototype system can verify various superscalar control designs of simple processors.

Critical properties of real-time embedded systems must be verified before these systems are deployed as failing to meet these properties may cause considerable property damages and/or human casualties. Although Statechart is one of the most popular languages for modeling behavior of real-time systems, proof systems and analysis tools for Statechart so far are in research and do not fully support the semantics of the original Statechart, or have limited capabilities for proving real-time properties. This paper introduces a toolset ASADAL/PROVER for verifying temporal properties of Statechart extended with justice and compassion properties. ASADAL/PROVER is composed of two subsystems, RTTL-Prover and Model-Checker. The RTTL-Prover converts Statechart specifications into real-time temporal logic (RTTL) formulas of Ostroff, and then checks if the formulas satisfy a temporal property (also in RTTL) using theorem proving techniques. The Model-Checker supports verification of a predefined set of real-time properties using a model checking technique. The RTTL-Prover can support verification of any real-time properties as long as they can be specified in RTTL and, therefore, messages generated by the tool are general and may not be of much help in debugging Statechart specifications. The Model-Checker, however, can provide detailed information for debugging. ASADAL/PROVER has been applied successfully to some experimental systems. One of on-going researches in this project is to apply the symbolic model-checking technique by[3]to support Statecharts with a much larger global-state space. We are also extending the types of temporal properties supported by the Model-Checker.

In ordinary digital signature schemes, anyone can verify signatures with signer's public key. However it is not necessary for anyone to be convinced a justification of signer's dishonorable message such as a bill. It is enough for a receiver only to convince outsiders of signature's justification if the signer does not execute a contract. On the other hand there exist messages such as official documents which will be first treated as limited verifier signatures but after a few years as ordinary digital signatures. We will propose a limited verifier signature scheme based on Horster-Michels-Petersen's authenticated encryption schemes, and show that our limited verifier signature scheme is more efficient than Chaum-Antwerpen undeniable signature schemes in a certain situation. And we will propose a convertible limited verifier signature scheme based on our limited verifier signature scheme, and show that our convertible limited verifier signature scheme is more efficient than Boyar-Chaum-Damg rd-Pedersen convertible undeniable signature schemes in a certain situation.

This paper introduces a new kind of false path, which is sensitizable but does not affect the decision of the maximum clock frequency. Such false paths exist in multi-clock operations controlled by waiting states, and the delay time of these paths can be greater than the clock period. This paper proposes a method to detect these waiting false paths based on the symbolic state traversal. In this method, the maximum allowable clock cycle of each path is computed using update cycles of each register.

A formal verification approach that combines verification based on binary decision diagrams (BDDs) and theorem-prover-based verification has been developed. This approach is called the incremental formal verification approach. It uses an incremental verifier based on BDDs and a conventional theorem-prover-based verifier. Inputs to the incremental verifier are specifications in higher-level descriptions given in terms of arithmetic expressions, lower-level design descriptions given in terms of Boolean expressions, and constraints. The incremental verifier limits the behavior of the design by using the constraints, and compares the partial behavior limited by the constraints with the specifications by using BDD-based Boolean matching. It also replaces the matched part of the lower design description with equivalent constructs in the higher descriptions. Successive uses of the incremental verifier with different constraints can produce higher design descriptions from the lower design descriptions in a step-by-step manner. These higher descriptions are then input to the theorem-prover-based verification which enables faster treatment of larger circuits. Preliminary experimental results show that the incremental verifier can successfully check the partial equivalence and replace the matched parts by higher constructs.

Backfire quadrifilar helical antennas combined with parasitic loops are investigated in detail, focusing on clarifying the function of parasitic loops. First, the basic property is examined for the case of one parasitic loop, and it is found that the loop behaves as a director when the circumferential length of the loop is nearly 0. 9λ, and a reflector when the circumferential length of the loop is nearly 1. 2λ provided the distance between the parasitic loop and the top plane of helical antennas is approximately 0. 1λ, where λ is the wavelength. Next, the function of the parasitic loop is investigated by comparing the current distributions on the helices and the loop with those on a monofilar helix with a ground plane. It is found that the function of the parasitic loop is quite different from that of the ground plane. Then, the case of two parasitic loops is examined, and it is shown that the use of two parasitic loops is very effective and simple measures to control the radiation pattern and gain of the backfire quadrifilar helical antennas. Finally, for this type of antennas with two parasitic loops, an example of structural parameters suited to the use in satellite communications is presented.

This paper proposes a top-down co-verification approach in the design of embedded systems composed of both hardware and software, for multimedia applications. In order to realize the optimized embedded system in cost, performance, power consumption and flexibility, hardware/software co-design becomes to be essential. In this top-down co-design flow, a target design is verified at three different levels: (1) algorithmic, (2) implementation, and (3) experimental. We have developed a methodology of top-down co-verification, which consists of the system level simulation at the algorithmic level, two type of co-simulations at the implementation level and the co-emulation at the experimental level. We have realized an environment optimized for verification performance by employing verification models appropriate to each verification stage and an efficient top-down environment by introducing the component logical bus architecture as the interface between hardware and software. Through actual application to a image compression and expansion system, the possibility of efficient co-verification was demonstrated.