This paper introduces methods to modify a buggy sequential gate-level circuit to conform to the specification. In order to preserve the optimization efforts, the modifications should be as small as possible. Assuming that the locations to be modified are given, our proposed method finds an appropriate set of fan-in signals for the patch function of those locations by iteratively calculating the state correspondence between the specification and the buggy circuit and applying a method for debugging combinational circuits. The experiments are conducted on ITC99 benchmark circuits, and it is shown that our proposed method can work when there are at most 30,000 corresponding reachable state pairs between two circuits. Moreover, a heuristic method using the information of data-path FFs is proposed, which can find a correct set of fan-ins for all the benchmark circuits within practical time.

A method for the exact cost performance analysis of autonomous discrete-time piecewise affine systems is presented. Cost performance refers to the average trajectory cost over the entire region of attraction of the origin. The trajectory cost is based on the infinite-horizon cost. First, a reverse reachability algorithm which constructs the explicit piecewise quadratic trajectory cost function over the entire region of attraction of the origin is presented. Then, an explicit expression for the integral of a quadratic function over a simplex of arbitrary dimension is derived. Thus, the piecewise quadratic trajectory cost function can be integrated exactly and efficiently in order to determine the cost performance of the system as a whole. This alleviates the need to perform a large number of simulations.

Petri nets are known as a modeling language for concurrent and distributed systems. In recent years, various object-oriented Petri nets were proposed, and we are proposing a kind of object-oriented Petri nets, called multi agent nets (MANs). In this letter, we consider the reachability analysis of MANs. We propose an algorithm for generating an abstract state space of a multi agent net, and report results of computational experiments.

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.

A requirement specification acquisition method combined with hypothesis-based reasoning and model reasoning is proposed for obtaining service specifications from the ambiguous and/or incomplete requirement specifications of communications services. Errors at an early stage of software development cost more to debug than those at a later stage. Specification acquisition is the most upstream development process. Nevertheless, the system support for specification acquisition is delayed compared with other development phases.' Users do not always have precise requirements. It is therefore inevitable that user requirements contain ambiguities, insufficiencies and even contradictions. Considering this, it is indispensable to support a specification completion method that derives service specifications from such problem requirements. This paper proposes a combined method to obtain consistent and complete specifications from such problem requirements. Communications service specifications can be described by specifying terminal behaviors which can be recognized from outside the communications system(s). Such specifications are described by a rule-based language. Requirement specifications usually have components that are ambiguous, incomplete, or even contradictory. They appear as rule description and/or missing rules. From such requirements, service specifications are obtained by using hypothesis-based reasoning on input requirements and existing service specifications. When existing specifications cannot be used to obtain complementary specifications, a communications service model is used to propose new rules. The proposed methods are implemented as a part of a communications software development system. The system enables non-experts in communications systems to define their own service specifications.

This paper discusses how to derive message sequence charts (MSCs) from a set of state transition descriptions. Recently, MSC notation has received much attention in the communications software field because it graphically shows system global behavior, So MSC handling techniques are being widely studied. These studies have recommended the design a system by a set of formal MSCs in the early stages of development and then to convert them into state transition descriptions. However, it is difficult to apply those results to existing communications software products. This is because these systems are designed based on state transition descriptions and there are no formal MSCs for them. In this paper, we propose a method of deriving MSCs based on optimized reachability analysis. This method generates MCSs that avoid state explosion. A case study using Q.931 protocol shows the feasibility of this method.

This paper proposes a test case generation method for testing concurrent programs as a black box. Typical applications are system testing for switching systems and inter-operability testing for OSI products. We adopt a two-step approach: first generate the control flow graph which represents global behaviors of a given concurrent program, and then apply conventional test case generation methods for the control flow graph. To generate a control flow graph without state space explosion, the black-box equivalence between system behaviors is introduced. The proposed algorithm generates a minimal control flow graph which consists of representatives of equivalence classes. Two practical techniques for the second step are discussed for a case study using a commercial digital PBX. The results show the feasibility of the proposed method.

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.