Many practical communication protocols provide priority service as well as ordinary service. In such a protocol, the protocol machines can initiate a priority service at most of the states. This characteristic leads an extreme increment of the number of state transitions on the protocol machines and causes state space explosion in verification of safety property of the protocol. This paper describes a method of constructing a communication protocol from composition of a subprotocol for ordinary service and that for priority service. This paper also presents a sufficient condition for a composed protocol to inherit safety property from the subprotocols. By using the composition method and the sufficient condition, the decision problem for safety property of the composed protocol can be reduced to those of the subprotocols. An experimental result of verification of a part of OSI session protocol is also described. The result shows that the method can reduce the computation time for verifying safety property to about 3% against the naive way.

An integrated platform INTEGRAL has been developed for developing large complex communication software systems. At the heart of INTEGRAL, a pair of graphical and textual specification languages, DISCOL (DIStributed Communication-Oriented Language), has been developed based on Petri nets. Around DISCOL, a wide variety of design and analysis tools have been integrated in coherent manner so that a seamless support from design to verification and testing are made available along with software life-cycle. The platform has been applied to the development of a PBX simulator named UICPBX. In the development, some real communication services have been fully specified with DISCOL. Such experiences have revealed the effectiveness of the proposed techniques.

The paper describes a parallel algorithm for the manipulation of binary decision diagrams on a shared memory multi-processor system. Binary decision diagrams are very efficient representations of logic functions, and are widely used in computer aided design of logic circuits. Logic operations on logic functions such as AND and OR are reduced to operations on binary decision diagrams representing these functions. Operations on binary decision diagrams are time-consuming in some cases, and a fast manipulation method is needed. As with the manipulation, we focus on the construction of a binary decision diagram from a logic formula, and devised a parallel algorithm for the construction. In the construction, there are many logic operations to be processed, and some of them can be processed in parallel. At first, we introduce an extraction method and a parallel-execution method for such parallelizable operations. This is the parallel execution method for an operation sequence (or a set of operations). To extract more parallelism, we introduce a dynamic expansion method of a logic operation. The dynamic expansion is a method to obtain sub-operations from a logic operation using the modified Shannon's expansion. These sub-operations are executed in parallel and the results of these sub-operations are merged to obtain the result of the original operation. Our parallel algorithm, which is based on the construction of shared binary decision diagrams with the negative edge and the operation cache, is implemented in C on a shared memory multi-processor system Sequent S-81 (CPU 80386 (16 MHz)28, 86.75MB), and applied to multiplier examples and ISCAS benchmarks. The speed-up ratio becomes 14 for multipliers, and becomes 11 for c1908 in ISCAS benchmarks.

In this paper we propose a new timing verification technique named coded time-symbolic simulation, CTSS. Our interest is on simulation of logic circuits consisting of gates whose delay is specified only by its minimum and maximum values. Conventional logic simulation based on min/max delay model leads to over-pessimistic results. In our new method, the cases of possible delay values of each gate are encoded by binary vectors. The circuit behavior for all the possible combinations of the delay values are simulated based on symbolic simulation by assigning Boolean variables to the binary vectors. This simulation technique can deal with logic circuits containing feedback loops as well as combinational circuits. We implemented an efficient simulator by using shared binary decision diagrams (SBDD's) as internal representation of Boolean functions. We also propose novel techniques of analyzing the results of CTSS.

This paper presents the EXM-algorithm, which locates multiple logic design errors in a combinational circuit with multiple output. The error possibility index and the six-valued simulation method have been enhanced to be applied to multiple output circuit. The algorithm locates multiple errors even if they belong to different cone circuits, and processes faster than the conventional EX-algorithm for circuits with the similar gate sizes. Experimental results have shown that the algorithm locates all errors at high hit ratio for ISCAS benchmark circuits and some other circuits.

This paper describes a verification scheme for service specifications and presents verification results for prototype system. Verified specifications are described by information sequence charts, which describe the communicating states between users and the messages between a user and a network. The verification scheme consists of two steps: macro sequence verification, which treats rough transitions of states, and transition procedure verification, which treats procedure of all messages. A prototype verification system demonstrates that this scheme can detect about 90% of errors in a specification within 4.4 seconds.

Recently, Burch et al. proposed symbolic model checking method to verify sequential machines formally. The method, which is based on logic function manipulation using binary decision diagram, can handle large sequential machines that cannot be handled by the conventional techniques. The expressive power of Computational Tree Logic (CTL), which was used by Burch et al., is not very powerful, for example, CTL cannot describe repetition of events. This papers shows an extension of the symbolic model checking algorithm to Branching time regular temporal logic (BRTL), which has been proposed by the authors as an improvement of CTL in terms of expressive power. The implemented verifier based on the proposed algorithm could verify behaviors of a microprocessor composed of approximately 1,600 gates and 68 flipflops.

Behavioral extraction from circuit description is a useful technique for logic design verification. We have proposed a technique of extraction from combinational circuits and developed a prototype system. To use this system practically, it is necessary to deal with sequential circuits. In this paper, we will present a new technique to extract behavioral descriptions from synchronous sequential circuits which include some flip-flops. Flip-flops are classified to two types. The one is a part of control registers. The other is a part of data registers. Behavior of the circuit with control registers is described by the state transition. Behavior of the circuit with data registers is described by the movement of data among registers. There are many circuits, as micro processors, which realize a function after some times of state transitions occurred. In such circuits, it is more important to abstract the function than to extract each state transition. We have progressed our system to extract such behaviors.

In this paper an approach to formal specification and verification of ISDN services in LOTOS is presented. As for specification, it is shown that LOTOS can be effectively applied to describe different levels of ISDN service specifications. At the higher level, only the external behaviour of the network is specified. On the other hand, at the lower level, specifications include the behaviour of network components such as switching systems, where each switching system can be specified independently of each other. Such specification style, proves suitable for verification of specifications by using the concepts of the simulation relation.

Plasmaless etching using ClF3 gas has been investigated on nitride films with different composition. For the sputter deposited and thermally grown silicon nitride films containing no hydrogen, the etch rate increases and the activation energy decreases with increase of the composition ratio of silicon to nitrogen between 0.75 and 1.3. This fact indicates that the etching is likely to proceed through the reaction between Si and ClF3. The native oxide on the silicon-nitride films can also be removed with ClF3 gas. Ultra-violet light irradiation from a low pressure mercury lamp remarkably accelerates the removal of the native oxide and the etch rate of the thermally grown silicon-nitride films. For the plasma deposited films, the etch rate is strongly accelerate with increasing hydrogen content in the films, but the activation energy hardly depends on the bounded hydrogen in the films, consistent with the results for Si etching.

Serious failures of the latest electronic equipments occur easily due to electrostatic discharge (ESD) , which can be caused frequently by the electrification phenomena of human-body walking on the floor. The number of the above damaging incidents has significantly been increasing with an increased use of integrated semiconductor elements with lower operation power. The most effective measures against the ESD consist in preventive ones, which are to obtain dynamic behaviors of the electric charge before the ESD happens, thereby preventing the charge accumulation. From this point of view, this paper describes new approaches for measurement of the static electricity directed toward preventing the ESD. First, a two-dimensional measurement method for visualizing charge distributions is described. This principle is based on visualizing the potential distribution induced in the array electrodes from the electrostatic fields. For showing usefulness of the visualization measurement, a prototype was built and attempts were made on the visualizations for the static electricity distributions of charged bodies. Second, a potential calculation of the human body charged by walking on the floor is described. A model was shown for analyzing the human-body potential on the floor, and the theoretical equation for describing the potential attenuation process was derived in the closed form in the Laplacian transformation domain. In order to obtain the typical half-life of the human-body potential, numerical computations were performed using a reverse Laplacian transformation. The experiments were also conducted for confirming the validity of the computed results. Finally, a new method is described for estimating dynamic behaviors of the occurrence charges of the human body electrified by walking-motions. Statistical measurements of the charges and potentials were made for the fundamental walking-motions specified here. The pace transitions of the potentials due to continuous walking and stepping were also measured and their results were explained from the electrification properties for the fundamental walking-motions.