JPH0458744B2 - - Google Patents

Description

DETAILED DESCRIPTION OF THE INVENTION (Field of Industrial Application) The present invention relates to a protocol verification method that inputs the specifications of a communication protocol, detects internal contradictions contained therein as specification errors, and outputs the detected specifications.

(Prior Art) With the recent advancement and diversification of telecommunications, software in communication equipment such as switching equipment and communication processing equipment is becoming larger and more complex. For this reason, it has become increasingly important to improve productivity in the development and maintenance of communication software.

One effective way to improve productivity in the development and maintenance of communications software is to accurately and accurately define the required specifications for communications software at an early stage of development and maintenance. The goal is to eliminate feedback work. Protocols, which define signal formats and procedures for transmitting and receiving various signals via communication lines, play an important role in communication software. Therefore, protocol verification technology that automatically detects logical contradictions or ambiguities in protocol specifications is important.

Traditionally, this type of protocol verification method is
In accordance with a given communication protocol specification, all combinations of operations and states that a communication system can take were sequentially enumerated and examined.

This conventional technique will be explained using FIGS. 2 and 3.

FIG. 2 is an example of a protocol to be verified, and is a diagram illustrating the protocol specifications of a communication system consisting of processes 1, 2, and 3. Here, the communication system may be, for example, a system in which processes 1 and 3 are terminal devices and process 2 is a switch, or processes 1, 2, and 3 may all be in one CPU. . That is, a processing unit that sends and receives signals to and from other functions (or may only send or receive signals) is called a process, and a plurality of processes that send and receive signals to and from each other are collectively called a communication system. FIG. 2 is an example of a protocol when there are three processes.

In FIG. 2, circles represent states and arrows represent transitions. The labels attached to the arrows also indicate the transmission or reception of a signal, with -a generally representing transmission of signal a, and +a representing reception of signal a. Therefore, process 1 takes A as its initial state, sends signal a to process 2 and transitions to state B, transitions to state C when it receives signal b from process 2, and sends signal c to process 2. It can be seen that the operation is performed in such a way as to return to the initial state A by transmitting . In this way, although the operation of each process can be understood relatively easily, it is not easy to determine whether there is a logical contradiction between processes 1, 2, and 3.

The conventional protocol verification technology described above is a state transition diagram of the entire communication system that sequentially executes all executable transitions from the initial state by sending or receiving one signal, and includes all reachable states. was created, and during the creation process, logical contradictions, or specification errors, were detected. FIG. 3 shows the result of applying this prior art to the protocol example shown in FIG. 2. This figure 3 is called a global transition diagram because it shows the state transition of the entire system. In addition, the status of each process is displayed in a circle, and this is called a global status.

First, in the initial global state (A ₁ , A ₂ , A ₃ ), -a in process 1 and process 3
-x is defined, but these are executable. In process 2, only reception of a is defined, but since signal a has not yet been sent from process 1, +a is not executable. As a result, the initial global state (A ₁ , A ₂ ,
In A ₃ ), the possible transitions are -a and -
x can be detected. Therefore, when we first test and execute the transition of -a, the global state (B, A,
A). If executable transitions are detected again in this state, there are +a and -x. For example, when +a is tested and executed, it becomes a global state (B, A, A).

On the other hand, in the initial global state (A, A, A), if we test and execute another possible transition - x, the global state (A, A, B)
becomes.

By repeating the above process as much as possible, the global state transition diagram shown in FIG. 3 can be obtained. By using FIG. 3 and FIG. 2, specification errors such as deadlock, (executable) undefined reception, and impossible transmission/reception can be detected. For example, in Figure 3, the global state (B, F, C)
is in a deadlock state because there is no executable transition for any process. In addition, in the global state (A, A, B) in FIG. 3, process 3 has already sent the signal x, so process 2 in FIG.
If reception of signal x+x is defined in state A of , it should be possible to execute this. This transition is the missing definition in FIG. 2 and is detected as an undefined reception.

Moreover, since FIG. 3 is the result of executing all executable transitions of the system, it can be said that the transitions in FIG. 2 that are not included in FIG. 3 are excessive. From this point of view, the signal reception in state C of process 3 +z
is detected as over-defined.

As mentioned above, the initial global state (A, A,
The protocol is verified by sequentially executing all executable transitions starting from A).

(Problems to be Solved by the Invention) In the above-mentioned conventional technology, all executable transitions are subject to inspection, so when the protocol becomes large-scale and complicated, the number of states and transitions increases. The amount of data has become enormous, the amount of processing, that is, the processing time has increased, and verification has become virtually impossible.

(Means for Solving the Problems) The present invention was made in view of the above-mentioned shortcomings of the conventional technology, and aims to provide a protocol verification method with a small amount of processing. The purpose of this system is to summarize the operations of communication systems to the extent that they do not cause any problems, and to enumerate and inspect the minimum necessary conditions and operations.

(Example) The principle of the present invention will be explained below, but before that, definitions and assumptions regarding the protocol, and terminology for explanation will be organized.

In this example, the specifications of the protocol to be verified are Q _i , O _i M _ij , succ (i, j=1,
..., N; N: number of processes).

Q _i : State set of process i.

O _i : Initial state of process i.

M _ij : A set of signals sent from process i to process j. However, M _ij =φ (empty set)
(i=j,...,N).

succ: A function that represents the state that a process takes as a result of transmitting and receiving signals in each state. succ (s, x) is the state s
A process in sends a signal x (x<
0) or after transition due to reception (x>0).

In addition, the following assumptions are made for the protocol to be verified.

The state to which each process transitions by sending and receiving signals is uniquely determined depending on the signal and the original state.

Each process has a signal reception buffer with a sufficiently large capacity for each partner process.

The order in which signals are received and transmitted between processes is the same as the order in which they are transmitted.

The state G of the entire system that communicates using the protocol is a combination of two terms S and C, that is, G=<S,
C>, and G is called a global state. Here, S=(s ₁ ,...s _N , C=(c ₁₁ , c ₁₂ ,..., c _NN ), s _i is the state of process i, and c _ij is the state sent from process i to process j. is the sequence of signals on the signal reception buffer that has not yet been received and processed.
Global state G where all signal reception buffers are empty
=<S,<ε>i,j _N ==1> is called a stable global state. In particular, the stable global state G=<<O _i >i _N ==1, <ε>i, including the initial state of each process,
j _N =1> is called the initial global state and is represented by G ₀ . In order to avoid misunderstandings, the global state may be expressed only by the states of individual processes.

In global state G, by sending or receiving one signal, another global state is changed.
When transitioning to G', the relationship between G and G' is expressed as G⊥G'. Furthermore, G reached by repeating such transitions from the initial global state G ₀ , i.e.
G such that G ₀ ⊥…⊥G is said to be reachable.

An ordered pair <s, x> consisting of a state s of a process and a signal x is defined as a signal transmission transition if x<0, and x
If >0, it is called a signal reception transition. When succ<s,x> is defined in a given protocol specification, <s,x> is called a defined transition or a defined send/receive.

A defined send <s, x>(x<0) is executable when there is a reachable global state that includes s as an element. Also defined reception <s, x>
(x>0) is executable when there is a reachable global state that includes s as an element and stores the signal x at the beginning of the corresponding signal reception buffer.

Based on the above preparations, errors in protocol specifications detected by the present invention are as follows.

Excessive signal definitions: Signal transmission/reception included in the protocol specification that cannot be executed.

Missing signal definition: undefined reception that is not included in the protocol specification but is viable.

Deadlock state: A global state in which state transitions are infeasible for all processes.

Next, the principle of the present invention will be explained. In the present invention, (1)
Divide the protocol specification hierarchically into a plurality of blocks with each process as a unit, and (2) create a block state transition diagram BSTD consisting of possible states and transitions for each block and check for errors. Remove redundant states and transitions when creating each BSTD. As a result, the number of transitions and states to be examined can be reduced, reducing processing time and the amount of memory required, thereby achieving the object of the present invention.

Examples of division of protocol specifications according to the present invention are shown in FIGS. 4 and 5. FIG _. 4 is a diagram showing an example of one division of the protocol specifications in _FIG . This shows the result of dividing into ₁₂ blocks. In FIG. 4(a), nodes represent processes, and branches represent defined transmission or reception of signals between the processes represented by the nodes at both ends. Also, Figure 4
(b) is the result of representing the division in (a) as a tree, with vertices,
Each endpoint corresponds to the entire system and each process, and the remaining nodes correspond to each block. Fifth
The figure shows another example of dividing a protocol specification. First, a protocol specification consisting of eight processes 1 to 8 is divided into block B ₁₁ consisting of processes 1 to 5 and block B 11 consisting of processes 6 to 8. ₁₂
The result of dividing B ₁₁ into block B ₂₁ consisting of processes 1 and 2 and block ₂₂ consisting of processes 3 to 5 is shown. After performing division in this way, it is also possible to repeat the division. Such division is called hierarchical division. In addition,
The entire original process may also be conveniently referred to as a block.

Level is used as a term to indicate hierarchy in hierarchical division.

The level of a block is the number of times the division is repeated on the original set of all processes to obtain the block. The level of a signal and signal transmission/reception transition is set to the level of the block having the maximum level value among the blocks containing two processes that transmit and receive the signal. Note that a level with a large level value is called a lower level, and a level with a small level value is called an upper level.

Here, the method of hierarchical division described above will be explained.

In general, the effects of the present invention become greater as the number of mutual operations between blocks due to signal transmission and reception is reduced in this division. Therefore, one possible strategy is to divide the blocks so that the number of signals defined to be transmitted and received between blocks is reduced.
Furthermore, another policy for dividing blocks may be to divide blocks so that the number of processes in other blocks having signals transmitted and received between blocks is reduced.

Next, a block state transition diagram in the present invention
We will explain how to create BSTD. The present invention creates BSTDs at all levels. Creation of each BSTD and
For example, the above-mentioned conventional technique is applied to error checking using BSTD. First, we will explain the creation order of BSTD.

In general, the BSTD of a block at each level is based on the BSTD of the block at the immediately lower level included in that block, which is regarded as a state transition diagram for each process. The global state transition diagram obtained by applying this method is created by using its BSTD.

On the other hand, in order to create each BSTD using the conventional technology, it is necessary to determine the feasibility of signal transitions of processes belonging to that block. Such signal transitions include those above and below that level. However, among these transitions, the feasibility of the receive transition that belongs to the higher level and the subsequent send/receive transitions cannot be determined by that block, but can only be determined by verification processing at the higher level to which the receive transition belongs. It is something. That is, it is impossible to create a BSTD for each level independently from the creation of BSTDs for other levels, and it is necessary to create all BSTDs in parallel. Here, "receiving belonging to a higher level" or "receiving a higher level"
Both have the same meaning and indicate that a process included in the block receives a signal transmitted from a process included in another block.

Therefore, in the present invention, when creating BSTD for each level, such upper level reception is once removed.
That is, it is assumed that such reception is not possible. Then, after the processing of that block is completed, the blocks at the upper level are processed in order, and if it is determined that the receive transition that is assumed to be impossible at the lower level is executable, then The lower-level BSTD created assuming that such a reception transition cannot be executed is updated to add that reception transition and a transition that can be executed subsequent to it.

Such updating of the lower level BSTD is repeated as long as a new executable reception is detected in creating (updating) the upper level BSTD. As a result of the above processing, BSTDs at each level are created in parallel and in stages.

As mentioned earlier, generally the BSTD of a block at level L is the level (L+
Create it based on the BSTD of block 1). However, before that, compression is performed to integrate the block states included in the BSTD of level (L+1) and remove block transitions between the combined block states to the extent that it does not interfere with the detection of logic errors as described above. Apply processing. Thereafter, a level L BSTD is created by applying the conventional technique to these compressed BSTDs. However, for the lowest level block for which there are no lower level blocks, the BSTD is created directly from the state transition diagram of the process belonging to that block. Note that the transmission/reception transitions below level L that were not removed by the compression process are
When creating higher level BSTDs, treat all transitions as immediately executable. Furthermore, hereinafter, transitions belonging to a level higher than the BSTD to be compressed will be referred to as inter-block transitions, and transitions below that level will be referred to as intra-block transitions.

The BSTD compression processing method is as follows. That is, the following processing is executed for each intra-block transition included in the block state transition diagram BSTD. Let the intra-block transition be T ₀ , and the transition source and destination block states be S1 and S2, respectively. At this time, the following processing is performed when the following conditions are satisfied and at least one of the following conditions is satisfied.

There are no transitions with the same label that have S1 and S2 as the transition source states.

S1 is reachable from S2 only by intrablock transitions.

There are no transitions other than T ₀ defined that have S2 as the destination state, or if they are defined, all of them are infeasible.

No transitions with S1 as the transition source state other than T ₀ are defined, or if they are defined, all of them are infeasible.

Among the block states reachable from S1, those for which an inter-block transition is defined using that state as the transition source state must be reachable from S2 only by intra-block transition.

Let A be the set of block states reachable from S1 for which inter-block transitions are defined, and let A be the set of block states reachable from S2 for which inter-block transitions are defined with this as the transition destination state. Let it be B. In this case, any block state belonging to A can be reached from each block state belonging to B only by intra-block transitions.

Remove _T0 and replace S1 and S2 with a new block state S12.

All transition source/transition destination states of a transition in which S1 and S2 are transition source/transition destination states are S12.

FIG. 6 illustrates the above compression process. In Figure 6, T11 and T12 are S1 and S, respectively.
2 as the destination state, also T21, T22
are transitions with S1 and S2 as transition source states, respectively. As can be seen from the figure, in general, if intra-block transition T ₀ is removed and S1 and S2 are integrated,
Transition T that enters S2 when creating BSTD of upper level
12, a non-existent transition sequence is added in which transition T21 exiting from S1 is executed, and as a result, there is a possibility that logical errors cannot be detected correctly. However, if a condition or condition is satisfied, such an executable transition sequence actually exists. Further, if one of the conditions ~ is satisfied, such an extra transition sequence will not be added.
Therefore, by applying the above compression processing, the upper level
It can be said that all the logical errors mentioned above can be detected by creating BSTD.

FIG. 7 is a flowchart showing the principle of the present invention explained above.

Hereinafter, the present invention will be explained in more detail using Examples.

FIG. 1 is a circuit diagram showing an embodiment of the present invention. In Fig. 1, 1 is a memory that stores protocol specifications given from the outside as shown in Fig. 2, and 2 is a 4th memory.
A memory stores the hierarchical division of the protocol specifications as shown in the figure, 3 is a register that stores the value of variable L representing the level of the block to be processed, 4 is a block state transition diagram BSTD of blocks at each level and verification results. A memory 5 stores detected specification errors, and a register 5 stores flags indicating the presence or absence of executable reception detected in the BSTD creation (update) process for each level.

11 is a circuit block that initializes the L value of register 3 and memory 4; 12 is a circuit block that updates the BSTD of each block at the level indicated by register 3; and 13 is a reception determined to be executable by circuit block 12. presence or absence and L in register 3
14 is a circuit block that increases the L value in register 3 by 1; 15 is a circuit block that checks whether the L value in register 3 is equal to 0; 16 is a value indicated by register 3. A circuit block 17 is a circuit block for decrementing the value of register 3 by 1 after compressing each BSTD of level 1, and a circuit block 17 for detecting infeasible transmission and reception.

Figure 8 shows the protocol specifications in Figure 2 in memory 1.
This shows the single storage format when storing data in . 9th and 10th
The figures show the example of protocol specification division shown in FIGS. 4 and 5 and the storage format for storing the maximum level value Lm in the memory 2, respectively. FIG. 11 shows one storage format when the BSTD shown in FIG. 12, which will be shown later, is stored in the memory 4.

FIG. 12 shows each BSTD obtained as a result of applying the example protocol of FIG. 2 to the embodiment of FIG. 1. The operation of the embodiment shown in Fig. 1 will be explained below using the examples shown in Figs. It is assumed that

In the circuit diagram of FIG. 1, the initialization block operates first. The initial setting block 11 accesses the memory 2, reads the maximum level value Lm in the division of the protocol specifications, and sends the value to the register 3. As a result, the variable L is set to Lm. In the example of FIGS. 2 and 4, Lm=1, and register 3 becomes 1. Next, circuit block 11 is connected to memory 4.
Access and initialize this. When the circuit block 11 completes the above operations, it becomes the circuit block 12.
Start.

The operation of circuit block 12 is as follows. Circuit block 12 first accesses register 3 and reads the value of variable L. Next, memory 2 is accessed, and if L=Lm, the process name included in each block of level L is accessed, and if L<Lm, the level (L+
1) Read the block name. Next, a block state transition diagram BSTD is created for each block at level L using the following procedure. Hereinafter, the block of level L to be processed will be referred to as B.

(a) Access memory 1 and input the state transition diagram of all processes included in block B.

(b) Access the memory 4 and input the BSTD of block B at that point. moreover,
When L<Lm, input the BSTD of the block at level (L+1) included in block B.

(c) Using the various information input in (a) and (b), update the BSTD of block B input in (b) using the conventional method. That is, when L=Lm, a global state transition diagram of block B is created based on the state transition diagram of each process included in block B. Furthermore, when L<Lm, the BSTD of level (L+1) included in block B is regarded as a process state transition diagram, that is, the block state of each of these BSTDs is regarded as a process state, and the transition between block states is regarded as an interprocess transition. Then, a global state transition diagram is created by applying conventional techniques. However, if there has been a level L reception determined to be executable in the past, a global state transition diagram is created to include such reception and subsequent executable transmission/reception transitions. The global state transition diagram created by the conventional method in this way becomes the BSTD of block B. Here, the global state and global transition correspond to the block state and block transition, respectively.

In this global state transition diagram creation process, all receptions at a level higher than L, that is, receptions where the other process is not included in block B, are treated as unexecutable.

Also, the process included in block B is 1
, the part of the state transition diagram of the process that is determined to be executable is transferred to block B.
BSTD.

(d) The BSTD generated as a result of the processing in (c) is stored in memory 4.
Output to. However, this BSTD includes the upper-level reception transitions that were treated as unexecutable in the process (c), and such reception transitions are marked for identification.

(e) Reset the level L flag in register 5.

(f) If there is a reception transition of level L that is newly determined to be executable in the process of (c), then L<Lm
If so, the BSTD of level (L+1) is assumed to be infeasible in the past such a reception transition.
Since I was creating a level (L+1)
Mark such receptions in BSTD with a special mark to indicate that they are actionable. and,
Output the BSTD of level (L+1) to the memory 4. In this case, below level (L+1)
Since it is necessary to further update BSTD, a flag corresponding to level L in register 5 is set.

In addition, in the process (c), when undefined reception that can be executed by the conventional method is detected, that information is also output to the memory 4. Also, when L=0, a block state that has no executable transmission/reception is a deadlock state. When a deadlock state is detected, that information is also output to the memory 4.

In the example of FIGS. 2 and 4, the above circuit block 12
The BSTD of block B ₁₁ and block B ₁₂ is
is created.

For block B ₁₁ , first, the state transition diagrams of processes 1 and 2 are input from memory 1 in (a). Since the memory 4 has been initialized, there is no information to be input in (a). Next, in (c), the BSTD of block _B11 is created using the conventional method based on the state transition diagram of process 1 and process 2.
The resulting BSTD is the part shown in FIG. 12 (1). In this figure, the thick dotted arrow ==+x
is a reception that belongs to a higher level, and was treated as unexecutable at the time of creating this BSTD.

On the other hand, as for block _B12 , the only process included in it is process 3. Therefore, the BSTD of block B ₁₂ is the reception +
This is the part excluding z. Figure 13(2) shows the BSTD portion of _B12 created in this way.

The data shown in Figure 13 is output to the memory 4, but at this time, as mentioned earlier, special marks are added to the upper level receptions +x and +z that were treated as infeasible when creating these BSTDs. These are also output.

Also, when creating the BSTD part in Figure 13,
For example, in the block state (B, D), an undefined reception that can execute +a is detected, and such undefined reception is also output to the memory 4.

Furthermore, when creating FIG. 13, since +a and +b were detected as executable reception, a flag corresponding to level L=1 in register 5 is set.

When the circuit block 12 completes the above operations, it starts the circuit block 13. The operation of circuit block 13 is as follows. Circuit block 13 accesses memory 2 and reads the value of Lm. Next, access register 3 and read the value of L. Furthermore, the register 5 is accessed and the level L flag is read. If the flag is set, that is, if circuit block 12 detects an executable reception of level L when updating the BSTD of the block of level L, the value of L is further checked and L<
If it is Lm, circuit block 14 is activated. Further, if the flag remains reset or if L=Lm, the circuit block 15 is activated.

In the example of FIGS. 2 and 4, since L=Lm (=1), the circuit block 15 is activated.

Circuit block 14 accesses register 3, reads the value of variable L, increments the value of L by 1, and transfers the result to register 3. Thereafter, circuit block 12 is activated.

Circuit block 15 first accesses register 3, reads the value of variable L, and determines whether the value of L is 0 or not. If the result of the determination is that L is not 0, the circuit block 16 is activated. If L is 0, circuit block 17 is activated.

In the example of FIGS. 2 and 4, since L=1, circuit block 16 is activated.

Circuit block 16 first accesses register 3 and reads the value of variable L. Next, access memory 2, read the block name of level L,
For each block, the block state transition diagram BSTD is compressed using the following procedure. Let B be the block of level L to be processed below.

(a) Access memory 1 and input the state transition diagram of all processes included in block B.

(b) Access the memory 4 and input the BSTD of block B at that time.

(c) Compress the BSTD of block B input in (b) using the information input in (a) and (b). That is,
It is checked whether the compression condition described above is satisfied for each intra-block transition included in the BSTD, and only when the compression condition is satisfied, that intra-block transition is deleted, and its transition source state and transition destination state are combine into one state.

(d) Output the compressed BSTD obtained in (c) to the memory 4.

(e) Decrease the value of L by 1 and output the result to register 3.

In the examples shown in FIGS. 2 and 4, there are blocks B ₁₁ and B ₁₂ as level 1 blocks, and the BSTD portion of block B ₁₁ includes an intra-block transition. By checking whether the conditions for compression hold for each of these and removing the transitions that hold, for example, block states (A, A), (B, A),
(B, B), (B, C), (C, C), (A, C) are combined into one block state. As a result of this compression process, the BSTD part of block B ₁₁ is
As shown in FIG. 13(1), there are only three block states S1, S2, and S3 and three types of block transitions +c, +a, and +x.

The above processing results are output to the memory 4. After that, the value of L becomes 0.

After completing the above operations, circuit block 16 activates circuit block 12.

The operation of circuit block 12 is as previously described. In the examples shown in FIGS. 2 and 4, L=0, so this time a BSTD of level 0, that is, block _B01 , is created. That is, it is stored in the memory 4. Based on the BSTD part of block B ₁₁ and the BSTD part of block B ₁₂ in Figure 13, the block
BSTD of B ₀₁ is created. The result is shown in Figure 13.
As shown in the BSTD part of (3). This BSTD
It is determined that level 0 reception+x is executable in the creation of the part. Therefore, a mark indicating executable is added to +x of the BSTD part of block B ₁₁ at level 1, and the BSTD part of block B ₁₁ updated in this way is stored in memory 1.
is output to. Also, a flag corresponding to level 0 in register 5 is set.

When circuit block 12 completes the above operations, circuit block 13 is activated. The operation of circuit block 13 is as described above. In the example shown in FIGS. 2 and 4, since the level L flag in the register 5 is set and L<Lm (L=0, Lm=1), the circuit block 14 is activated.

The operation of the circuit block 14 is as described above, and in the examples shown in FIGS. 2 and 4, the value of L is added by 1 to become 1. Thereafter, circuit block 12 is activated again.

The operation of the circuit block 12 is as already explained, and in the example shown in Figs. 2 and 4, the BSTD of the level 1 block B ₁₁ is updated this time, and the BSTD of the block B 11 in Fig. 13 (1) is updated.
BSTD part is added.

Thereafter, circuit blocks 16 and 14 are activated repeatedly, and circuit block 12 is activated each time. As a result, the BSTD part in Figure 13,
, are created in order, and the BSTD shown in FIG. 13 is completed. At this time, L=0, and circuit block 17 is activated by circuit block 15.

Circuit block 17 accesses memory 1 to input all transmit and receive transitions included in the protocol specification. It also accesses the memory 4 and inputs the BSTD of all blocks. Then, compare the information on the two and select which of the transmission/reception transitions obtained from memory 1.
Those that are not included in the BSTD are output to the memory 4 as unexecutable transmission/reception.

In the examples shown in FIGS. 2 and 4, transition +z defined in process 3 is detected as an unexecutable transition.

In the above embodiment, the conventional method explained using FIGS. 2 and 3 was applied to create the block state transition diagram of the blocks at each level, but it is also possible to apply other methods. For example, “Global state transition batch processing method” (Patent application 1982-192491
17th)) “Process-specific state transition expansion method” (Tokugan Sho
59-271938 (December 25, 1981)) can also be applied.

(Effects of the Invention) As explained in detail above, the method according to the present invention divides a given protocol specification into a plurality of blocks with each process as a unit, creates a state transition diagram for each block, and checks for specification errors. do. Therefore, compared to the conventional method, the number of processes processed simultaneously is small, and as a result, both the number of states and the number of transitions generated are reduced. As a result, compared to conventional methods, the method proposed in this application significantly reduces the amount of processing required for verification processing, and also significantly reduces the memory capacity required to store global state transition diagrams, etc. The advantage is that it can be done.

[Brief explanation of the drawing]

Fig. 1 is a block diagram showing an embodiment of the present invention, Fig. 2 is a protocol to be verified, Fig. 3 is a global transition diagram, Figs. 4 and 5 are diagrams showing an example of division of protocol specifications, Fig. 6 7 is a flowchart showing the operation of the present invention, FIG. 8 is a diagram showing an example of the storage format of the protocol specifications in FIG. 2 in the memory 1, and FIGS. 9 and 10. stores each protocol specification division example and its maximum level value Lm in memory 2.
11 is an example of a BSTD storage format, and FIG. 12 is a diagram showing each BSTD obtained by applying the protocol example of FIG. 2 to the embodiment of FIG. 1.

Claims (1)

[Claims] 1. In a protocol verification circuit that receives as input a protocol specification that defines the signal format and procedure for transmission and reception in a communication system, and detects and outputs logical errors in the protocol specification, the protocol specification given from the outside is stored. A second memory that stores protocol specifications hierarchically divided into multiple blocks for each process, and a third memory that stores variable values representing the level of the block to be processed. and a fourth memory that stores specification errors detected as a result of block state transition diagrams and verification of blocks at each level; a fifth memory for accumulating a flag indicating the block status; initial setting means for initializing the variable value and the fourth memory; block state transition diagram updating means for updating the block state transition diagram; and reception determined to be executable. a first inspection means for inspecting the presence or absence of a variable and a variable value; an addition means for increasing the variable value by 1; and a second inspection means for inspecting whether the variable value is equal to 0 or not.
a compression means for reducing the variable value by 1 after compressing each block state transition diagram of the level of the variable value; and an error checking means for detecting infeasible transmission/reception. split verification circuit.