JPH0458744B2 - - Google Patents

Description

【発明の詳細な説明】 （産業上の利用分野） 本発明は、通信プロトコルの仕様を入力し、そ
れに含まれる内部矛循を仕様誤りとして検出し出
力するプロトコル検証方式に関する。

（従来の技術） 近年の電気通信の高度化・多様化に伴い、交換
機・通信処理装置等の通信機器におけるソフトウ
エアは大規模化・複雑化する一方である。このた
め通信ソフトウエアの開発・保守における生産性
を向上させることは益々重要となつてきた。

通信ソフトウエアの開発・保守における生産性
を向上させる一つの有力な方策は、通信ソフトウ
エアの要求仕様を開発・保守の早い段階で正確に
かつ過不足なく定義することにより、それ以後の
段階からのフイードバツク的な作業をなくすこと
である。通信ソフトウエアの中で重要な位置を占
めるものとして、通信回線を介して各種の信号を
送受するための信号形式や手順を規定するプロト
コルがある。従つて、プロトコルの仕様に論理的
矛循やあいまいさがあつた場合、これを自動的に
検出するプロトコル検証技術が重要となる。

従来、この種のプロトコル検証方式としては、
与えられた通信プロトコル仕様に従つて、通信シ
ステムがとり得る動作および状態のすべての組合
せを順次列挙し、検査するものであつた。

この従来技術を第２図、第３図を用いて説明す
る。

第２図は、検証しようとするプロトコルの一例
であつて、プロセス１，２および３からなる通信
システムのプロトコル仕様を図示したものであ
る。ここで、通信システムとは、例えばプロセス
１および３が端末装置、プロセス２が交換機であ
るシステムであつてもよいし、また、プロセス
１，２，３がともに一つのCPU内にあつてもよ
い。すなわち、他の機能と信号の送受信（送信ま
たは受信だけであつてもよい）を行う処理単位を
プロセスと呼び、互いに信号の授受を行う複数の
プロセスを総称して通信システムと呼ぶ。第２図
はプロセス数３の場合のプロトコルの一例であ
る。

第２図において、丸印は状態を、矢印は遷移を
表わす。また矢印に付けられたラベルは信号の送
信又は受信を示し、一般に−ａは信号ａの送信
を、また＋ａはａの受信を表わす。従つて、プロ
セス１はＡを初期状態として、プロセス２に対し
信号ａを送信して状態Ｂに遷移し、プロセス２か
ら信号ｂを受信したとき状態Ｃに遷移し、プロセ
ス２に対して信号ｃを送信して初期状態Ａに戻る
ように動作することが分かる。このように、各プ
ロセスの動作は比較的容易に理解できるが、プロ
セス１，２，３の相互間に論理矛循があるか否か
を判定することは容易でない。

前述したプロトコル検証の従来技術とは、一つ
の信号の送信又は受信による実行可能な遷移を初
期状態から遂一すべて順次に実行し、到達可能な
状態を全て含むような通信システム全体の状態遷
移図を作成し、その作成過程で論理矛循、すなわ
ち仕様誤りを検出していた。第２図のプロトコル
例に、この従来技術を適用した結果を第３図に示
す。この第３図はシステム全体の状態遷移を示す
ことからグローバル遷移図と呼ぶ。また、状態
は、丸印の中に各プロセスの状態が表示され、こ
れをグローバル状態と呼ぶ。

まず、初期グローバル状態（A₁，A₂，A₃）に
おいては、プロセス１における−ａとプロセス３
における−ｘが定義されているが、これらは実行
可能である。プロセス２においてはａの受信のみ
が定義されているが、信号ａはプロセス１から未
だ送信されていないので、＋ａは実行不可能であ
る。この結果、初期グローバル状態（A₁，A₂，
A₃）において実行可能な遷移としては、−ａと−
ｘが検出できる。そこで先ず−ａの遷移について
テストし実行するとグローバル状態（Ｂ，Ａ，
Ａ）となる。この状態で再度実行可能な遷移を検
出すると、＋ａと−ｘとがある。このうち例えば
＋ａについてテストし実行するとグローバル状態
（Ｂ，Ａ，Ａ）となる。

一方、初期グローバル状態（Ａ，Ａ，Ａ）にお
いて、もう一つの実行可能な遷移−ｘについてテ
ストし実行するとグローバル状態（Ａ，Ａ，Ｂ）
となる。

以上の処理を可能な限りくり返すことにより第
３図のグローバル状態遷移図を得ることができ
る。第３図と第２図を用いることにより、デツド
ロツク、（実行可能）未定義受信、実行不可能送
受信等の仕様誤りを検出することができる。例え
ば、第３図で、グローバル状態（Ｂ，Ｆ，Ｃ）
は、どのプロセスについても実行可能遷移がない
ためデツドロツク状態となる。また、第３図のグ
ローバル状態（Ａ，Ａ，Ｂ）では、プロセス３が
既に信号ｘを送信したので、第２図のプロセス２
の状態Ａで信号ｘの受信＋ｘが定義されていれば
これを実行することが可能なはずである。この遷
移は第２図に不足している定義であり、未定義受
信として検出される。

また、第３図は、システムの実行可能な全ての
遷移を実行した結果であるから、第３図に含まれ
ない第２図の遷移は過剰であるといえる。この観
点からプロセス３の状態Ｃにおける信号受信＋ｚ
が過剰な定義として検出される。

以上のように、初期グローバル状態（Ａ，Ａ，
Ａ）から実行可能な遷移を遂一すべて順次に実行
することによりプロトコルの検証が行われる。

（発明が解決しようとする問題点） 上述した従来技術によつては、全ての実行可能
な遷移を検査の対象とするため、プロトコルが大
規模化・複雑化した場合、状態数や遷移数が膨大
となり、処理量すなわち処理時間が増大し、実質
的に検証が不可能となつていた。

（問題点を解決するための手段） 本発明は、上述した従来技術の欠点に鑑みなさ
れたもので、処理量の少ないプロトコル検証方式
を提供することを目的とし、その特徴は、仕様誤
りを検出するのに支障ない範囲で通信システムの
動作を一括し、必要最小限の状態と動作を列挙し
て検査することにある。

（実施例） 以下に、本発明の原理を説明するが、その前に
プロトコルに関する定義と仮定、および説明のた
めの用語について整理しておく。

本実施例では、検証対象とするプロトコルの仕
様は、以下に示すQ_i，O_iM_ij，succ（ｉ，ｊ＝１，
…，Ｎ；Ｎ：プロセスの個数）の４項の組み合せ
で与えられるものとする。

Q_i：プロセスｉの状態集合。

O_i：プロセスｉの初期状態。

M_ij：プロセスｉからプロセスｊに送る信号の
集合。ただしM_ij＝φ（空集合）
（ｉ＝ｊ，…，Ｎ）とする。

succ：プロセスが各状態で信号を送受信するこ
とにより遷移した結果とる状態を表わ
す関数で、succ（ｓ，ｘ）は、状態ｓ
にあるプロセスが信号ｘの送信（ｘ＜
０）又は受信（ｘ＞０）により遷移し
た後の状態を表わす。

また、検証対象とするプロトコルに対し、以下
の仮定を設ける。

信号の送受により各プロセスが遷移する先の
状態は、その信号と元の状態に応じて一意に定
まる。

各プロセスは、容量が十分大きな信号受信用
バツフアを相手プロセス別に持つ。

プロセス相互間で送受する信号の受信順序は
送信順序と同一である。

プロトコルを用いて通信するシステム全体の状
態ＧをＳとＣの２項の組み合せ、即ちＧ＝＜Ｓ，
Ｃ＞で定義し、Ｇをグローバル状態と呼ぶ。ここ
で、Ｓ＝（s₁，…s_N，Ｃ＝（c₁₁，c₁₂，…，c_NN）で
あり、s_iはプロセスｉの状態、c_ijはプロセスｉか
らプロセスｊに送出されたが未が受信処理されて
いない信号受信バツフア上の信号の系列である。
信号受信バツフアがすべて空のグローバル状態Ｇ
＝＜Ｓ，＜ε＞ｉ，ｊ_N ＝＝１＞安定グローバル状
態と呼ぶ。特に各プロセスの初期状態を含む安定
グローバル状態Ｇ＝＜＜O_i＞ｉ_N ＝＝１，＜ε＞ｉ，
ｊ_N ＝１＞を初期グローバル状態と呼びG₀で表わ
す。尚、誤解することがない場合には、グローバ
ル状態を個々のプロセスの状態のみで表わすこと
もある。

グローバル状態Ｇにおいて、一つの信号を送信
或は受信することにより別のグローバル状態
G′に遷移するときＧとG′の関係をＧ⊥G′で表わ
す。更に、初期グローバル状態G₀からこのよう
な遷移をくり返すことにより到達するＧ、即ち
G₀⊥…⊥ＧであるＧは到達可能であるという。

あるプロセスの状態ｓと信号ｘより成る順序対
＜ｓ，ｘ＞を、ｘ＜０であれば信号送信遷移、ｘ
＞０であれば信号受信遷移と呼ぶ。与えられたプ
ロトコル仕様にsucc＜ｓ，ｘ＞が定義されている
とき、＜ｓ，ｘ＞を定義済遷移又は定義済送／受
信と呼ぶ。

定義済送信＜ｓ，ｘ＞（ｘ＜０）は、ｓを要素
として含む到達可能なグローバル状態が存在する
とき実行可能である。また定義済受信＜ｓ，ｘ＞
（ｘ＞０）は、ｓを要素として含みかつ該当する
信号受信バツフアの先頭に信号ｘを蓄積している
到達可能グローバル状態が存在するとき実行可能
である。

以上の準備に基づいて、本発明が検出するプロ
トコル仕様の誤りを示すと以下の通りである。

信号定義の過剰：プロトコル仕様に含まれる
信号の送受信の内実行し得ないもの。

信号定義の不足：プロトコル仕様に含まれな
いが実行可能である未定義受信。

デツドロツク状態：すべてのプロセスについ
て状態遷移が実行不可能であるグローバル状
態。

次に本発明の原理を説明する。本発明では、(1)
プロトコル仕様をプロセスを単位として階層的に
複数個のブロツクに分割し、(2)各ブロツクについ
てそれがとり得る状態、および遷移から構成され
るブロツク状態遷移図BSTDを作成して誤りを検
査する。各BSTDを作成するとき、冗長な状態お
よび遷移を削除する。その結果、検査する遷移数
と状態数を削減できるので、処理時間並びに所要
メモリ量が減少し、本発明の目的が達成される。

本発明によるプロトコル仕様の分割例を第４図
と第５図に示す。第４図は第２図のプロトコル仕
様の一分割例を示す図で、プロセス１〜３より構
成されるシステムB₀₁を、プロセス１と２とから
構成されるブロツクB₁₁と残りのプロセス３から
構成されるブロツクB₁₂とに分割した結果を表わ
す。第４図(a)で節点はプロセスを、また枝はその
両端の節点が表わすプロセス間に信号の送信又は
受信が定義されていることを表わす。また第４図
(b)は同図(a)の分割を木で表わした結果で、頂点、
各端点がそれぞれシステム全体、各プロセスに対
応し、残りの節点が各ブロツクに対応する。第５
図は別のプロトコル仕様の分割例を示す図であ
り、１〜８の８個のプロセスから構成されるプロ
トコル仕様を、まずプロセス１〜５から成るブロ
ツクB₁₁とプロセス６〜８から成るブロツクB₁₂
とに分割し、さらにB₁₁をプロセス１と２から成
るブロツクB₂₁とプロセス３〜５から成るブロツ
ク₂₂に分割した結果を表わす。このように一旦分
割を行つた後、さらに分割をくり返すこともでき
る。このような分割を階層的分割と呼ぶ。なお、
元のプロセス全体も便宜的にブロツクと呼ぶこと
がある。

階層的分割における階層を示す用語としてレベ
ルを用いる。

ブロツクのレベルは、そのブロツクを得るため
に元の全プロセス集合に対して施した分割のくり
返し回数とする。信号および信号送受信遷移のレ
ベルは、その信号を送受する二つのプロセスを含
むブロツクの内、レベル値が最大であるブロツク
のレベルとする。なお、レベル値が大きいものを
下位レベル、逆にレベル値が小さいものを上位レ
ベルと呼ぶ。

ここで以上で述べた階層的分割の仕方を説明す
る。

一般に本発明による効果はこの分割において信
号の送受信によるブロツク間の相互動作が少ない
ほど大きくなる。したがつて例えばブロツク間で
送受する様に定義された信号の個数が少なくなる
様に分割する事が一つの方針として考えられる。
さらに、ブロツク分割の別の方針としては、ブロ
ツク間で送受する信号を持つ他ブロツクのプロセ
ス数が少なくなるように分割するという考え方も
採れる。

次に、本発明におけるブロツク状態遷移図
BSTDの作成法を述べる。本発明ではすべてのレ
ベルのBSTDを作成する。各BSTDの作成並びに
BSTDを用いた誤り検査には、例えば先に述べた
従来技術を応用する。まずBSTDの作成順序を説
明する。

一般に、各レベルのブロツクのBSTDは、その
ブロツクに含まれるすぐ下位のレベルのブロツク
のBSTDをプロセス毎の状態遷移図とみなし、つ
まり下位レベルのブロツク状態をプロセス状態と
みなし、それらに従来技術を適用することにより
得られるグローバル状態遷移図をそのBSTDとす
ることにより作成する。

一方、従来技術で各BSTDを作成するには、そ
のブロツクに属すプロセスが持つ信号遷移の実行
可能性を判定する必要がある。そのような信号遷
移には、そのレベルより上位のものも下位のもの
も含まれる。しかし、これらの遷移の内、上位レ
ベルに属す受信遷移およびそれ以降の送受信遷移
の実行可能性はそのブロツクでは判定できず、そ
の受信遷移が属す上位のレベルでの検証処理によ
つて初めて判定できるものである。即ち、各レベ
ルのBSTDの作成は、他のレベルのBSTDの作成
と独立して行うことは不可能であり、全BSTDの
作成を並行して進める必要がある。ここで、「上
位レベルに属す受信」や「上位レベルの受信」
は、いずれも同じ意味であり、他ブロツクに含ま
れるプロセスから送信される信号を当該ブロツク
に含まれるプロセスが受信することを表す。

そこで、本発明では各レベルのBSTDを作成す
る場合一旦このような上位レベルの受信を除く、
即ち、そのような受信は実行不可能であると仮定
する。そして、そのブロツクの処理が終了した
後、順に上位レベルのブロツクを処理することと
し、その処理で下位レベルで実行不可能と仮定し
た受信遷移が実行可能であると判定された場合に
は、そのような受信遷移を実行不可能と仮定して
作成した下位レベルのBSTDを更新してその受信
遷移およびそれに引き続き実行できる遷移を付加
する。

このような下位レベルBSTDの更新は、上位レ
ベルのBSTDの作成（更新）において新たな実行
可能受信を検出する限りくりかえし行う。以上の
処理の結果、各レベルのBSTDは並行して段階的
に作成されることとなる。

先に述べたように、一般にレベルＬのブロツク
のBSTDはそのブロツクに含まれるレベル（Ｌ＋
１）のブロツクのBSTDを基にして作成する。し
かし、その前に先に示した論理誤りの検出に支障
のない範囲で、レベル（Ｌ＋１）のBSTDに含ま
れるブロツク状態を統合し、それら結合されたブ
ロツク状態間のブロツク遷移を除去するという圧
縮処理を施す。そして、その後、圧縮されたこれ
らBSTDに従来技術を適用することによりレベル
ＬのBSTDを作成する。ただし、下位レベルのブ
ロツクが存在しない最下位レベルのブロツクにつ
いては、そのブロツクに属すプロセスの状態遷移
図から直接BSTDを作成する。尚、圧縮処理で除
去されなかつたレベルＬ以下の送受信遷移は、Ｌ
より上位のレベルのBSTDを作成する場合にはす
べて直ちに実行可能な遷移として扱う。また、以
下では、圧縮の対象となるBSTDより上位のレベ
ルに属す遷移をブロツク間遷移、またそのレベル
以下の遷移をブロツク内遷移と呼ぶ。

BSTDの圧縮処理法は次に示す通りである。即
ち、ブロツク状態遷移図BSTDに含まれる各ブロ
ツク内遷移について以下の処理を実行する。ブロ
ツク内遷移をT₀、その遷移元ブロツク状態・遷
移先ブロツク状態をそれぞれS1・S2とする。こ
のとき以下に示す条件が成立し、かつ〜の
条件の内少なくとも一つが成立するとき、と
の処理を施す。

S1，S2を遷移元状態とする同一ラベルの遷
移が存在しないこと。

S1がブロツク内遷移のみによつてS2から到
達可能であること。

S2を遷移先状態とする遷移がT₀以外一切定
義されていない、または定義されている場合そ
れらがすべて実行不可能なこと。

S1を遷移元状態とする遷移がT₀以外一切定
義されていない、または定義されている場合そ
れらがすべて実行不可能なこと。

S1から到達可能なブロツク状態の内、それ
を遷移元状態とするブロツク間遷移が定義され
ているものは、必らずS2からブロツク内遷移
のみによつて到達可能なこと。

S1から到達可能なブロツク状態の内ブロツ
ク間遷移が定義されているものの集合をＡと
し、S2に到達可能なブロツク状態の内それを
遷移先状態とするブロツク間遷移が定義されて
いるものの集合をＢとする。このとき、Ａに属
す任意のブロツク状態が、Ｂに属す各ブロツク
状態からブロツク内遷移のみにおいて到達可能
であること。

T₀を除去するとともにS1とS2を一つの新し
いブロツク状態S12で置き替える。

S1・S2を遷移元／遷移先状態とする遷移の
遷移元／遷移先状態をすべてS12とする。

第６図は上記の圧縮処理を図示したものであ
る。第６図でＴ１１，Ｔ１２はそれぞれＳ１，Ｓ
２を遷移先状態とする遷移、またＴ２１，Ｔ２２
は、それぞれＳ１，Ｓ２を遷移元状態とする遷移
である。同図から分かるように、一般にブロツク
内遷移T₀を除去してＳ１とＳ２を統合すると、
上位のレベルのBSTD作成時にＳ２に入る遷移Ｔ
１２を実行した後、Ｓ１から出る遷移Ｔ２１を実
行するという実在しない遷移系列を付加し、その
結果、論理誤りを正しく検出できなくなる可能性
が生じる。しかし、条件またはが成立すれば
このような実行可能な遷移系列が元々実際に存在
する。また、条件〜の一つが成立すればその
ような余分な遷移系列が付加されることはない。
従つて、上記の圧縮処理を施して上位レベルの
BSTDを作成することにより先に述べた論理誤り
をすべて検出することが言える。

第７図は、以上で説明した本発明の原理をフロ
ーチヤートで示したものである。

以下、実施例を用いてさらに詳しく本発明を説
明する。

第１図は本発明の一実施例を示す回路図であ
る。第１図で、１は外部から与えられる第２図の
如きプロトコル仕様を蓄積するメモリ、２は第４
図の如きプロトコル仕様の階層的分割を蓄積する
メモリ、３は処理対象とするブロツクのレベルを
表わす変数Ｌの値を蓄積するレジスタ、４は各レ
ベルのブロツクのブロツク状態遷移図BSTDおよ
び検証の結果検出した仕様誤りを蓄積するメモ
リ、５はBSTD作成（更新）処理で検出した実行
可能受信の有無をレベルごとに示すフラグを蓄積
するレジスタである。

１１は、レジスタ３のＬ値およびメモリ４を初
期設定する回路ブロツク、１２はレジスタ３で示
されるレベルの各ブロツクのBSTDを更新する回
路ブロツク、１３は回路ブロツク１２で実行可能
と判定された受信の有無およびレジスタ３内のＬ
値を検査する回路ブロツク、１４はレジスタ３内
のＬ値を１だけ増やす回路ブロツク、１５はレジ
スタ３内のＬ値が０に等しいか否かを検査する回
路ブロツク、１６はレジスタ３の示す値のレベル
の各BSTDを圧縮処理した後、レジスタ３の値を
１だけ減じる回路ブロツク、１７は実行不可能送
受信を検出する回路ブロツクである。

第８図は、第２図のプロトコル仕様をメモリ１
に蓄積する場合の一蓄積形式を示す。第９，１０
図はそれぞれ第４，５図のプロトコル仕様分割例
およびその最大レベル値Lmをメモリ２に蓄積す
る場合の一蓄積形式を示す。第１１図は後で示す
第１２図のBSTDをメモリ４に蓄積する場合の一
蓄積形式を示す。

第１２図は第２図のプロトコル例を第１図の実
施例に適用した結果得られる各BSTDを示す。以
下、第２，４図の例を用いて第１図の実施例の動
作を説明するが、プロトコル仕様およびその分割
はそれぞれ第８図，第９図の形式で既にメモリ
１，２に蓄積されているものとする。

第１図の回路図では、最初に初期設定ブロツク
が動作する。初期設定ブロツク１１はメモリ２に
アクセスし、プロトコル仕様の分割における最大
レベル値Lmを読みとり、その値をレジスタ３に
送出する。この結果、変数ＬはLmに設定され
る。第２，４図の例ではLm＝１でありレジスタ
３は１となる。次に回路ブロツク１１はメモリ４
にアクセスし、これを初期設定する。回路ブロツ
ク１１は以上の動作を終えると回路ブロツク１２
を起動する。

回路ブロツク１２の動作は次の通りである。回
路ブロツク１２は、まずレジスタ３にアクセスし
て、変数Ｌの値を読みとる。次に、メモリ２にア
クセスし、Ｌ＝LmであればレベルＬの各ブロツ
クに含まれるプロセス名を、またＬ＜Lmであれ
ばレベルＬの各ブロツクに含まれるレベル（Ｌ＋
１）のブロツク名を読みとる。次に、レベルＬの
各ブロツクについて以下の手順によりブロツク状
態遷移図BSTDを作成する。以下、処理の対象と
なるレベルＬのブロツクをＢとする。

(ア) メモリ１にアクセスして、ブロツクＢに含
まれる全プロセスの状態遷移図を入力する。

(イ) メモリ４にアクセスして、その時点におけ
るブロツクＢのBSTDを入力する。さらに、
Ｌ＜LmのときはブロツクＢに含まれるレベ
ル（Ｌ＋１）のブロツクのBSTDを入力す
る。

(ウ) (ア)と(イ)で入力した各種情報を用いて(イ)で
入
力したブロツクＢのBSTDを、従来方式によ
り更新する。即ち、Ｌ＝Lmのときは、ブロ
ツクＢに含まれる各プロセスの状態遷移図を
基にして、ブロツクＢのグローバル状態遷移
図を作成する。またＬ＜Lmのときはブロツ
クＢに含まれるレベル（Ｌ＋１）のBSTDを
プロセス状態遷移図とみなし、つまり、これ
ら各BSTDのブロツク状態をプロセス状態と
みなし、ブロツク状態間遷移をプロセス間遷
移とみなして、従来の技術を適用することに
よりグローバル状態遷移図を作成する。ただ
し、過去に実行可能と判定されたレベルＬの
受信があれば、そのような受信およびそれ以
降実行可能な送受信遷移を含むようグローバ
ル状態遷移図を作成する。このようにして従
来方式により作成されたグローバル状態遷移
図がブロツクＢのBSTDとなる。ここでグロ
ーバル状態、グローバル遷移がそれぞれブロ
ツク状態、ブロツク遷移に対応する。

このグローバル状態遷移図作成処理におい
て、Ｌより上位のレベルの受信、即ち、相手
プロセスがブロツクＢに含まれないような受
信はすべて実行不可能なものとして扱う。

また、ブロツクＢに含まれるプロセスが１
個のときは、そのプロセスの状態遷移図の内
実行可能と判定される部分をブロツクＢの
BSTDとする。

(エ) (ウ)の処理の結果生成したBSTDをメモリ４
に出力する。たゞしこのBSTDは、(ウ)の処理
で実行不可能として扱つた上位レベルの受信
遷移までを含めたものであり、そのような受
信遷移には識別のための印を付けておく。

(オ) レジスタ５内のレベルＬのフラグをリセツ
トする。

(カ) (ウ)の処理であらたに実行可能と判定された
レベルＬの受信遷移があつた場合、Ｌ＜Lm
であれば過去にそのような受信遷移を実行不
可能なものとしてレベル（Ｌ＋１）のBSTD
を作成していたので、レベル（Ｌ＋１）の
BSTDにおけるそのような受信に実行可能で
あることを示す特別な印を付ける。そして、
レベル（Ｌ＋１）のBSTDをメモリ４に出力
する。この場合、レベル（Ｌ＋１）以下の
BSTDをさらに更新する必要があるので、レ
ジスタ５内のレベルＬに相当するフラグをセ
ツトする。

なお、(ウ)の処理で、従来方式により実行可能な
未定義受信を検出したときは、その情報を併せて
メモリ４に出力する。また、Ｌ＝０のとき、実行
可能送受信を一切持たないブロツク状態はデツド
ロツク状態である。デツドロツク状態を検出した
ときはその情報を併せてメモリ４に出力する。

第２，４図の例では、以上の回路ブロツク１２
の動作によりブロツクB₁₁とブロツクB₁₂のBSTD
が作成される。

ブロツクB₁₁については、まず(ア)により、プロ
セス１と２の状態遷移図をメモリ１から入力す
る。メモリ４は初期設定された後なので、(イ)で入
力される情報はない。次に、(ウ)において、プロセ
ス１とプロセス２の状態遷移図を基にして、従来
方式によりブロツクB₁₁のBSTDが作成される。
その結果得られるBSTDは第１２図(1)のの部分
である。この図で、点線の太い矢印＝＝＋ｘ
は、上位レベルに属す受信であり、このBSTDを
作成する時点では実行不可能なものとして扱つた
ものである。

一方、ブロツクB₁₂については、それに含まれ
るプロセスはプロセス３のみである。従つて、ブ
ロツクB₁₂のBSTDは、プロセス３の状態遷移図
の中で実行可能と判定することができない受信＋
ｚを除いた部分となる。第１３図(2)のが、この
ようにして作成されたB₁₂のBSTD部分である。

メモリ４には第１３図のとが出力される
が、このとき先に述べた通りこれらBSTDを作成
する際実行不可能として扱われた上位レベルの受
信＋ｘ，＋ｚに特別なマークが付加されてこれら
も併せて出力される。

また、第１３図のBSTD部分を作成する際、
例えばブロツク状態（Ｂ，Ｄ）において＋ａを実
行可能な未定義受信を検出し、そのような未定義
受信も併せてメモリ４に出力する。

さらに、第１３図を作成する際、実行可能な
受信として＋ａおよび＋ｂを検出したので、レジ
スタ５内のレベルＬ＝１に相当するフラグをセツ
トする。

回路ブロツク１２は以上の動作を終えると回路
ブロツク１３を起動する。回路ブロツク１３の動
作は次の通りである。回路ブロツク１３はメモリ
２にアクセスしてLmの値を読みとる。次にレジ
スタ３にアクセスしてＬの値を読みとる。さらに
レジスタ５にアクセスしてレベルＬのフラグを読
みとる。そのフラグがセツトされている場合、即
ち、回路ブロツク１２においてレベルＬのブロツ
クのBSTDを更新する際レベルＬの実行可能受信
を検出した場合は、さらにＬの値を検査し、Ｌ＜
Lmであれば回路ブロツク１４を起動する。ま
た、前記フラグがリセツトされたまま、あるいは
Ｌ＝Lmの場合は回路ブロツク１５を起動する。

第２，４図の例では、Ｌ＝Lm（＝１）である
ため、回路ブロツク１５が起動される。

回路ブロツク１４は、レジスタ３にアクセスし
て変数Ｌの値を読みとり、Ｌの値を１だけ増加さ
せてその結果をレジスタ３に転送する。その後回
路ブロツク１２を起動する。

回路ブロツク１５は、まず、レジスタ３にアク
セスして変数Ｌの値を読みとり、Ｌの値が０であ
るか否か判定する。判定の結果Ｌが０でなければ
回路ブロツク１６を起動する。またＬが０であれ
ば、回路ブロツク１７を起動する。

第２，４図の例ではＬ＝１であるので回路ブロ
ツク１６が起動される。

回路ブロツク１６は、まずレジスタ３にアクセ
スして変数Ｌの値を読みとる。次にメモリ２にア
クセスして、レベルＬのブロツク名を読みとり、
それら各ブロツクについて以下の手順によりその
ブロツク状態遷移図BSTDを圧縮処理する。以下
処理の対象となるレベルＬのブロツクをＢとす
る。

(ア) メモリ１にアクセスしてブロツクＢに含ま
れる全プロセスの状態遷移図を入力する。

(イ) メモリ４にアクセスしてその時点における
ブロツクＢのBSTDを入力する。

(ウ) (ア)と(イ)で入力した情報を用いて(イ)で入力
し
たブロツクＢのBSTDを圧縮する。即ち、
BSTDに含まれる各ブロツク内遷移について
先に述べた圧縮条件が成立するか否か検査
し、圧縮条件が成立するときのみ、そのブロ
ツク内遷移を削除し、その遷移元状態と遷移
先状態とを一つの状態にまとめる。

(エ) (ウ)で得られた圧縮BSTDをメモリ４に出力
する。

(オ) Ｌの値を１だけ減少させ、その結果をレジ
スタ３に出力する。

第２，４図の例では、レベル１のブロツクとし
てブロツクB₁₁とB₁₂とがあるが、その内ブロツ
クB₁₁のBSTD部分にブロツク内遷移が含まれ
ている。これらの各々について圧縮のための条件
が成立するか否か検査し、成立する遷移を除去す
ると、例えばブロツク状態（Ａ，Ａ），（Ｂ，Ａ），
（Ｂ，Ｂ），（Ｂ，Ｃ），（Ｃ，Ｃ），（Ａ，Ｃ）が一
つのブロツク状態にまとめられる。このような圧
縮処理の結果、ブロツクB₁₁のBSTD部分は、
第１３図(1)に示す通り、Ｓ１，Ｓ２およびＳ３の
３個のブロツク状態と＋ｃ，＋ａ，＋ｘの３種のブ
ロツク遷移のみとなる。

以上の処理結果はメモリ４に出力される。その
後Ｌの値は０となる。

回路ブロツク１６は以上の動作を終えると回路
ブロツク１２を起動する。

回路ブロツク１２の動作は先に説明した通りで
ある。第２，４図の例ではＬ＝０となつているの
で、今度はレベル０即ちブロツクB₀₁のBSTDが
作成される。即ち、メモリ４内に蓄蓄積されてい
る。第１３図のブロツクB₁₁のBSTD部分とブ
ロツクB₁₂のBSTD部分を基にして、ブロツク
B₀₁のBSTDが作成される。その結果は第１３図
(3)のBSTD部分に示す通りである。このBSTD
部分の作成においてレベル０の受信＋ｘが実行
可能であると判定される。従つて、レベル１のブ
ロツクB₁₁のBSTD部分の＋ｘに、実行可能で
あることを示すマークが付加され、このように更
新されたブロツクB₁₁のBSTD部分がメモリ１
に出力される。また、レジスタ５内のレベル０に
相当するフラグをセツトする。

回路ブロツク１２が以上の動作を終えると回路
ブロツク１３が起動される。回路ブロツク１３の
動作は先に説明した通りである。第２，４図の例
では、レジスタ５内のレベルＬのフラグがセツト
されており、かつＬ＜Lm（Ｌ＝０，Lm＝１）で
あるため、回路ブロツク１４が起動される。

回路ブロツク１４の動作は先に述べた通りであ
り、第２，４図の例では、Ｌの値が１加算されて
１となる。その後、再び回路ブロツク１２が起動
される。

回路ブロツク１２の動作は既に説明した通りで
あり、第２，４図の例では、今回はレベル１のブ
ロツクB₁₁のBSTDが更新され、第１３図(1)の
BSTD部分が追加される。

以下、回路ブロツク１６と１４が交互にくり返
し起動されるが、その都度回路ブロツク１２が起
動される。その結果、第１３図のBSTD部分，
，が順に作成され、第１３図に示すBSTDが
完成する。このときＬ＝０であり、回路ブロツク
１５により回路ブロツク１７が起動される。

回路ブロツク１７は、メモリ１にアクセスして
プロトコル仕様に含まれる全ての送受信遷移を入
力する。また、メモリ４にアクセスして全ブロツ
クのBSTDを入力する。そして、両者の情報を比
較し、メモリ１から得た送受信遷移の内、どの
BSTDにも含まれないものを実行不可能送受信と
してメモリ４に出力する。

第２，４図の例では、プロセス３に定義されて
いる遷移＋ｚが実行不可能な遷移として検出され
る。

以上の実施例では、各レベルのブロツクのブロ
ツク状態遷移図の作成には第２，３図を用いて説
明した従来方式を応用したが、他の方式を応用す
ることも可能である。例えば“グローバル状態遷
移一括処理方式”（特願昭59−192491（昭和59年９
月17日））“プロセス別状態遷移展開法”（特願昭
59−271938（昭和59年12月25日））を応用すること
もできる。

（発明の効果） 以上詳細に説明したように、本発明による方式
は、与えられたプロトコル仕様をプロセスを単位
として複数のブロツクに分割し、ブロツク毎に状
態遷移図を作成して仕様誤りを検査する。このた
め、従来方式に比較すると、同時に処理するプロ
セス数が少なく、その結果生成される状態数およ
び遷移数は共に減少する。その結果、従来方式に
比較して、本出願による方式は検証処理に必要と
なる処理量が大幅に減少するとともに、グローバ
ル状態遷移図等を蓄積するために必要となるメモ
リの容量を大幅に削減することができるという利
点がある。

【図面の簡単な説明】

第１図は本発明の実施例を示すブロツク図、第
２図は検証対象プロトコル、第３図はグローバル
遷移図、第４図と第５図はプロトコル仕様の分割
例を示す図、第６図は圧縮処理を示す図、第７図
は本発明の動作を示すフローチヤート、第８図は
第２図のプロトコル仕様のメモリ１への蓄積形式
の例を示す図、第９図と第１０図は各プロトコル
仕様分割例及びその最大レベル値Lmをメモリ２
に蓄積する形式例、第１１図はBSTDの蓄積形式
例、第１２図は第２図のプロトコル例を第１図の
実施例に適用して得られる各BSTDを示す図であ
る。

Claims (1)

1. 【特許請求の範囲】 １ 通信システムにおける送受信の信号形式や手
   順を規定するプロトコル仕様を入力として、該プ
   ロトコル仕様の有する論理誤りを検出・出力する
   プロトコル検証回路において、 外部から与えられるプロトコル仕様を蓄積する
   第１のメモリと、 プロトコル仕様をプロセスを単位として階層的
   に複数のブロツクに分割して蓄積する第２のメモ
   リと、 処理対象とするブロツクのレベルを表す変数値
   を蓄積する第３のメモリと、 各レベルのブロツクのブロツク状態遷移図及び
   検証の結果検出した仕様誤りを蓄積する第４のメ
   モリと、 ブロツク状態遷移図の作成及び更新処理で検出
   した実行可能な受信の有無をレベルごとに示すフ
   ラグを蓄積する第５のメモリと、 前記変数値と第４のメモリを初期設定する初期
   設定手段と、 ブロツク状態遷移図を更新するブロツク状態遷
   移図更新手段と、 実行可能と判断された受信の有無及び変数値を
   検査する第１の検査手段と、 前記変数値を１増やす加算手段と、 前記変数値が０に等しいか否かを検査する第２
   の検査手段と、 前記変数値のレベルの各ブロツク状態遷移図を
   圧縮処理した後前記変数値を１減じる圧縮手段
   と、 実行不可能送受信を検出する誤り検査手段とか
   らなることを特徴とするプロトコルの分割検証回
   路。