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.

A computational model for security verification of cryptographic protocols is proposed. Until most recently, security verification of cryptographic protocols was left to the protocol designers' experience and heuristics. Though some formal verification methods have been proposed for this purpose, they are still insufficient for the verification of practical real-time cryptographic protocols. In this paper we propose a new formalism based on a term rewriting system approach that we have developed. In this model, what and when the saboteur can obtain is expressed by a first-order term of a special form, and time-related concepts such as the passage of time and the causality relation are specified by conditional term rewriting systems. By using our model, a cryptographic protocol which was shown to be secure by the BAN-logic is shown to be insecure.

Verification of responsive communication protocols is to determine whether they can recover to a normal state within a predetermined time, even when they enter an abnormal state due to any fault. In this paper, we propose a new verification method for responsive communication protocols using virtual system states, each of which represents several system states. Next, in order to evaluate the effectiveness of the new method, we develop a verification tool based on the proposed method. Then we apply the tool to a broadcasting protocol and measure several metrics on the tool. The experimental results show that (1) the number of system states, (2) the amount of memory used by the tool, and (3) the execution time of the tool, can be drastically reduced.

Geometric region method is one of the techniques to handle real-time systems which have potentially infinite state spaces. However, the original geometric region method gives incorrect results for the CTL model checking of time Petri nets. In this paper, we discuss the sufficient condition for the geometric region graphs to be correct with respect to the CTL model checking of time Petri nets, and then propose a technique to partition given geometric regions so that the graphs satisfy the sufficient condition. Finally, we implement the proposed algorithm, and compare it with the other methods by using small examples.

Requirements engineering refers to activities of gathering and organizing customer requirements and system specifications, making explicit representations of them, and making sure that they are valid and accounted for during the course of the design lifecycle of software. One very popular software development practice is the incremental development practice. The incremental development refers to practices that allow a program, or similarly specifications, to be developed, validated, and delivered in stages. The incremental practice is characterized by its depth-first process where focuses are given to small parts of the system in sequence to fair amounts of detail. In this paper, we present a development and validation of specifications in such an incremental style using a tool called ASADAL, a comprehensive CASE tool for real-time systems. ASADAL supports incremental and hierarchical refinements of specifications using multiple representational constructs and the evolving incomplete specifications can be formally tested with respect to critical real time properties or be simulated to determine whether the specifications capture the intended system behavior. In particular, we highlight features of ASADAL's specification simulator, called ASADAL/SIM, that plays a critical role in the incremental validation and helps users gain insights into the validity of evolving specifications. Such features include the multiple and mixed level simulation, real-value simulation, presentation and analysis of simulation data, and variety of flexible simulation control schemes. We illustrate the overall process using an example of an incremental specification development of an elevator control system.

A simple method of compensating the DC drift of LiNbO3 Mach-Zehnder intensity modulators for very high speed optical transmission systems is proposed. This method adds low frequency perturbation to the modulator driving signal, and controls the bias voltage using the detected envelope of the modulator output signal. The control circuit is successfully demonstrated to work with less than a 0. 1-dB power penalty.

We propose a new method for verifying synchronous circuits using the Boyer-Moore Theorem Prover (BMTP) based on an efficient use of induction. The method contains two techniques. The one is the representation method of signals. Each signal is represented not as a waveform, but as a time parameterized function. The other is the mechanical transformation of the circuit description. A simple description of the logical connection of the components of a circuit is transformed into such a form that is not only acceptable as a definition of BMTP but also adequate for applying induction. We formalize the method and show that it realizes an efficient proof.

A family of nonce-based authentication and key distribution protocols based on the trusted third-party model are proposed which are not only efficient on the view points of computation and communication, but also secure against on-line and off-line password guessing attacks. A new concept of implicit or indirect challenge-response authentication which can be used to combine the processes of identify authentication and data integrity assurance during key distribution and to make the entire protocol be more concise and efficient is introduced in this paper. In the proposed family of protocols, specific protocol can be chosen such that the secure session key to be distributed is selected by specific participant in the protocol. Detailed security analyses of every protocols are given.

We propose an on-line writer verification method to improve the reliability of verifying a specific system user. Most of the recent research focus on signature verification especially in the field of on-line writer verification. However, signature verification has a serious problem in that it will accept forged handwriting. To overcome this problem, we have introduced a text-indicated writer verification method. In this method, a different text including ordinary characters is used on every occasion of verification. This text can be selected automatically by the verification system so as to reflect the specific writer's personal features. A specific writer is accepted only when the same text as indicated by the verification system is inputted, and the system can verify the writer's personal features from the inputted text. Moreover, the characters used in the verification process can be different from those in the enrolment process. This method makes it more difficult to get away with forged handwriting than the previous methods using only signatures. We also discuss the reliability of the proposed method with some simulation results using handwriting data. From these simulation results, it is clear that this method keeps high reliability without the use of signatures.

Verification of timed bisimulation equivalence is generally difficult because of the state explosion caused by concrete time values. In this paper, we propose a verification method to verify timed bisimulation equivalence of two timed processes using a symbolic technique similar to [1]. We first propose a new model of timed processes, Alternating Timed Symbolic Labelled Transition System (A-TSLTS). In an A-TSLTS, each state has some parameter variables, whose values determine its behaviour. Each transition in an A-TSLTS has a quard predicate. The transition is executable if and only if its guard predicate is true underspecified parameter values. In the proposed method, we can obtain the weakest condition for a state-pair in a finite A-TSLTS, which the parameter values in the weakest condition must satisfy to make the state-pair be timed bisimulation equivalent.

In this paper we propose a method of formal verification of totally self-checking (TSC) properties of combinational circuits using logic function manipulation. We show that the problem of verification of TSC properties can be transformed to a satisfiability problem of decision functions formed from characteristic functions of a circuit's output code words. Then the problem can be solved using binary decision diagrams (BDD). Experimental results show the effectiveness of the proposed method.

In order to apply formal design verification, it is necessary to describe formally and correctly the specification of the circuit under verification. Especially when we apply conventional OBDD-based logic comparison method for verifying combinational circuits, another correct" logic circuits or Boolean formulae must be given as the specification. It is desired to develop an efficient automatic design verification method which interprets specification that can be described easier. This paper provides a new verification method which is useful for combinational circuits such as arithmetic circuits. The proposed method efficiently verifies whether a designed circuit satisfies a specification given by recurrence equations. This enables us to describe easily an error-free specification for arithmetic circuits. To perform verification efficiently using an ordinary OBDD package, an efficient truth-value rotation algorithm is developed. The truthvalue rotation algorithm efficiently generates an OBDD representing f(x + 1 (mod 2n)) from a given OBDD representing f(x). By experiments on SPARC station 10 model 51, it takes 180 secs to generate an OBDD for designed circuit of 23-bit square function, and additional 60 secs is sufficient to finish verifying that it satisfies the specification given by recurrence equations.

Flurorinated liquid crystal compounds having fluorophenyl, difluorophenyl and trifluorophenyl moieties combined with ester linkages, 1,2-ethylenes and covalent bonds were prepared and checked for their physical properties i.e. mesophases, dielectric and optical anisotropy. viscosity, pretilt angle and threshold voltage. By introducing fluorine atom(s) into the molecules, optical anisotropy and threshold voltage decreased, though the nematic temperature range diminished. The investigated compounds were all chemically stable and by using the compounds nematic liquid crystalline mixtures having low threshold voltage, low viscosity, large optical anisotropy and wide nematic ranges which were suitable for AM-LCDs, could be obtained.

We have devised a polynomial time algorithm to decide the security of cryptographic protocols formally under certain conditions, and implemented the algorithm on a computer as a supporting system for deciding the security. In this paper, a useful approach is presented to decide security problems which do not satisfy some of the above-mentioned conditions by using the system. For its application, we consider a basic security problem of Kerberos protocol, whether or not an enemy can obtain the session key between a client and a server by using any information not protected in communication channels and using any operation not prohibited in the system. It is shown that Kerberos is secure for this problem.

Exploring enormous state graphs represented implicitly by ordered binary decision diagrams (OBDDs) is one of the most successful applications of OBDDs. However, our worst-case analysis of implicit graph representations by OBDDs shows that there are cases where OBDD representations are not optimal and require more space than adjacency lists. As an improvement, we propose a new type of BDDs, called Patricia BDDs, which are capable of implicit representation of graphs while their worst-case sizes are kept equal or less than adjacency lists and OBDDs.

A data-flow program net is a graph representation of data-flow programs consisting of three types of nodes, AND-node, OR-node and SWITCH-node, which represent arithmetic/logical, data merge and context switch operations respectively. Token self-cleanness is an important property of a data-flow program and is such that if date-flow programs satisfy the property then a date-flow computer can efficiently withdraw copies from given programs during executions. In this paper, we classify program nets into SWITCH-less, OR-less and general nets, and analyse structures of data-flow program nets to propose verification methods of token self-cleanness by investigating token numbers appearing on the edges. As a result, a necessary and sufficient condition is proposed for SWITCH-less data-flow program nets and sufficient conditions are given for OR-less and general data-flow program nets.

This paper describes the results obtained of a prototype system, VeriProc/1, based on an algorithm we first presented in [13] which can prove the correctness of pipelined processors automatically without pipeline invariant, human interaction, or additional information. 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. The performance is independent of not only data width but also memory size. Detailed analysis of CPU time is presented. Further, don't-care forcing using additional data easily prepared by the user can improve performance.

This paper describes a newly developed sensing scheme with a bit-by-bit program verify technique for NAND flash disk systems. This sensing scheme achieves good noise immunity for large capacitive coupling between bitlines, and makes NAND flash memories operable for flexible power supply voltages including both 3.3V and 5V. A highly reliable read operation is performed for power supply voltages above 3V and a bitline-bitline coupling ratio below 50%. The sensing scheme also achieves an intelligent page copy function with 20% reduction in time and without external buffers and CPU resources.

This paper deals with on-line signature verification. A signature is obtained as a sequence of x, y-coordinates of pen-tip movement and writing pressure. The features of a signature are derived from the coordinates and the writing pressure and are decomposed into two principal features, shape and motion, using the DP-matching technique. We found that each point of a signature varies each time to some degree. However, the degrees of local variations subject to points, as some points are relatively stable and do not vary much while some of them are not. In this paper, we propose to incorporate weighted local variations based on the stability of each point so as to evaluate the difference of two signatures locally as well as globally. The dissimilarity measures are presented with respect to the corresponding features and are combined into one for efficient verification. In addition to the x, y-coordinates, the writing pressure is also considered to be part of shape. Experiments were carried out with a database which consists of 300 genuine signatures and 300 forgeries collected from 10 subjects. The effectiveness of incorporating the weighted local variation is shown by the experimental results. It contributes to an average increase in the correct verification rate as the correct verification rate increased 1.0% and was found to be 98.7%.

This paper presents implicit representation of binary decision diagrams (implicit BDDs) as a new effecient data structure for Boolean functions. A well-known method of representing graphs by binary decision diagrams (BDDs) is applied to BDDs themselves. Namely, it is a BDD representation of BDDs. Regularity in the structure of BDDs representing certain Boolean functions contributes to significant reduction in size of the resulting implicit BDD repersentation. Since the implicit BDDs also provide canonical forms for Boolean functions, the equivalence of the two implicit BDD forms is decided in time proportional to the representation size. We also show an algorithm to maniqulate Boolean functions on this implicit data structure.