JPS61208945A - プロトコルの分割検証回路 - Google Patents

Abstract

(57)【要約】本公報は電子出願前の出願データであるた
め要約のデータは記録されません。

Description

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

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

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

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

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

第２図は、検証しようとするプロトコルの一例であって
、プロセスＬ２および３からなる通信システムのプロト
コル仕様を図示したものである。

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

第２図において、丸印は状態を、矢印は遷移を表わす。

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

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

先ず、初期グローバル状態（Ａ・Ａ・Ａ）において、即
実行可能な遷移を検出すると、プロセス１における一ａ
とプロセス３におけるーＸである。

プロセス２においてはａの受信のみであシ、かつ信号ａ
はプロセス１から末だ送信されていないので、＋ａは実
行不可能である。そこで先ず−ａの遷移についてテスト
するとグローバル状態（Ｂ、Ａ。

Ａ）となる。この状態で再度即実行可能な遷移を検出す
ると、＋ａと−Ｘとがある。このうち例えば＋ａについ
てテストするとグローバル状態（Ｂ。

Ｂ、Ａ）となる。

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

以上の処理を可能な限り＜シ返すことにより第３図のグ
ローバル状態遷移図を得ることができる。

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

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

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

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

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

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

本実施例では、検証対象とするプロトコルの仕様は、以
下に示すＱｉ　、Ｏｉ　＋Ｍｉｊ＋　５ｕｃｃ（ｉ＋ｊ
＝＝１１・・・・ＮＵＮ：プロセスの個数）の４項の組
み合せで与えられるものとする。

Ｑｉ’プロセスｉの状態集合。

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

Ｍｉｊ：プロセスｉからプロセスｊに送る信号の集合。

ただしＭｉｉ＝Φ（全集合）（ｉ＝１゜・・・、Ｎ）と
する。

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

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

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

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

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

プロトコルを用いて通信するシステム全体の状態ＧをＳ
とＣの２項の組み合せ、即ちＧ＝＜Ｓ、Ｃ＞で定義し、
Ｇをグローバル状態と呼ぶ。ここで、Ｓ＝（町１℃８　
Ｎ　）　−〇＝（（！１１１　Ｃ１２＋　＝０１０ＮＮ
）でありｓ　Ｓｌはプロセスｉの状態、ｃｉｊはプロセ
スｉからプロセスｊに送出されたが末だ受信処理されて
いない信号受信バッファ上の信号の系列である。信号受
信バッファがすべて空のグローバル状態Ｇ＝＜Ｓ・、Ｎ くε＞ｉ、Ｊ＝１＞を安定グローバル状態と呼ぶ。特に
各プロセスの初期状態を含む安定グローバル状態Ｇ＝ぐ
Ｑｉ＞ｉ＝１．くε）ｉ、ｊ＝１）を初期２グローバル
状態と呼びＧｏで表わす。尚、誤解することがない場合
には、グローバル状態を個々のプロセスの状態のみで表
わすこともある。

クローバル状態Ｇにおいて、一つの信号を送信或は受信
することにより別のグローバル状態げに遷移するときＧ
とσの関係をＧドσで表わす。更に、初期グローバル状
態−為らこのような遷移を（シ返すことにより到達する
Ｇ、即ちＧ。旨・・・トＧであるＧは到達可能であると
いう。

あるプロセスの状態Ｓと信号Ｘよ構成る順序対くｓ、Ｘ
〉を、ｘ＜ｏであれば信号送信遷移、Ｘ＞０であれば信
号受信遷移と呼ぶ。与えられたプロトコル仕様に５ｕｃ
ｃ（ｓ　＋　ｘ）が定義されているとき、と。、ｖ′″
−＞冬中丼溶１玖マは常丼溶喜／尋稽シ睡ジ一定義済送
信くＳ・ｘ＞（ｘ＜Ｏ）は、Ｓを要素として含む到達可
能なグローバル状態が存在するとき実行可能である。ま
た定義済受信（ｓ　、　ｘ）（ｘ＞０　）は。

Ｓを要素として含みかつ該当する信号受信バッファの先
頭に信号Ｘを蓄積している到達可能グローバル状態が存
在するとき実行可能である。

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

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

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

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

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

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

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

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

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

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

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

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

一方、従来技術で各ＢＳＴＤを作成するには、そのブロ
ックに属すプロセスが持つ信号遷移の実行可能性を判定
する必要がある。そのような信号遷移には、そのレベル
よシ上位のものも下位のものも含まれる。しかし、これ
らの遷移の内、上位レベルに属す受信遷移およびそれ以
降の送受信遷移の実行可能性はそのブロックでは判定で
きず、その受信遷移が属す上位のレベルでの検証処理に
よって初めて判定できるものである。即ち、各レベルの
ＢＳＴＤの作成は、他のレベルのＢＳＴＤの作成と独立
して行うことは不可能で１、全ＢＳＴＤの作成を並行し
て、進める必要がある。

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

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

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

ＢＳＴＤの圧縮処理法は次に示す通りである。即ち、ブ
ロック状態遷移図ＢＳＴＤに含まれる各ブロック内遷移
について以下の処理を実行する。ブロック内遷移をＴｏ
、その遷移光ブロック状態・遷移先ブロック状態をそれ
ぞれＳｌ・Ｓ２とする。このとき以下に示す条件■が成
立し、かつ■〜■の条件の肉食なくとも一つが成立する
とき、■と■の処理を施す。

■　３１．Ｓ２を遷移元状態とする同一ラベルの遷移が
存在しないこと。

■　Ｓｌがブロック内遷移のみによって８２から到達可
能であること。

■　Ｓ２を遷移先状態とする遷移がＴｏ以外−切定義さ
れていない、または定義されている場合それらがすべて
実行不可能なこと。

■　Ｓｌを遷移元状態とする遷移がＴｏ以外−切定義さ
れていない、または定義されている場合それらがすべて
実行不可能なこと。

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

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

■　Ｔｏを除去するとともに８１と８２を一つの新しい
ブロック状態Ｓ１２で置き替える。

■　Ｓｌ・Ｓ２を遷移元／遷移先状態とする遷移の遷移
元／遷移先状態をすべて８１２とする。

第６図は上記の圧縮処理を図示したものである。

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

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

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

第１図は本発明の一実施例を示す回路図である。

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

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

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

第１１図は後で示す第１２図のＢＳＴＤをメモリ４に蓄
積する場合の一蓄積形式を示す。

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

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

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

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

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

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

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

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

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

（３）　レジスタ５内の７ベルＬのフラグをリセットす
る。

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

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

第２・４図の例では、以上の回路ブロック１２の動作に
よジブロックＢｌｌとブロックＢ１２のＢＳＴＤが作成
される。

ブロックＢｕについては、まず（７）により、プロセス
１と２の状態遷移図をメモリ１から入力する。

メモリ４は初期設定された後なので、（イ）で入力され
る情報はない。次に、（つ）において、プロセス１とプ
ロセス２の状態遷移図を基にして、従来方式によりブロ
ックＢｎのＢＳＴＤが作成される。その結果得られるＢ
ＳＴＤは第１２図（１）の■の部分である。

この図で、点線の太い矢印＝＝今＋又は、上位レベルに
属す受信でアシ、このＢＳＴＤを作成する時点では実行
不可能なものとして扱ったものである。

一方、ブロックＢ１２については、それに含まれるプロ
セスはプロセス３のみである。従って、ブロックＢＩ２
のＢＳＴＤは、プロセス３の状態遷移図の中で実行可能
と判定することができない受信＋２を除いた部分となる
。第１３図（２）の■が、このようにして作成されたＢ
１２のＢＳＴＤ部分である。

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

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

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

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

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

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

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

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

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

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

（イ）メモリ４にアクセスしてその時点におけるブロッ
クＢのＢＳＴＤを入力する。

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

ＧＴ−）（つ）で得られた圧縮ＢＳＴＤをメモリ４に出
力する。

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

第２，４図の例では、レベル１のブロックとしてブロッ
クＢ１１とＢ１２とがあるが、その内ブロックＢｉｔの
ＢＳＴＤ部分■部分口ック内遷移が含まれている。

これらの各々について圧縮のだめの条件が成立するか否
か検査し、成立する遷移を除去すると、例えばブロック
状態（Ａ、Ａ）、（Ｂ、Ａ）、（Ｂ、Ｂ）。

（Ｂ　、Ｃ）　、　（Ｃ、Ｃ）　、　（Ａ、Ｃ）が一つ
のブロック状態にまとめられる。このような圧縮処理の
結果、ブロックＢｌｌのＢＳＴＤ部分■部分口１３図（
１）に示す通り、Ｓｌ・ＳｌおよびＳ３の３個のブロッ
ク状態と＋Ｃ＋−ａ＋＋Ｘの３種のブロック遷移のみと
なる。

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

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

回路ブロック１２の動作は先に説明した通シである。第
２，４図の例ではＬｍ０となっているので、今度ヒレベ
ル０即ちブロック１３ｏｔのＢＳＴＤが作成される。即
ち、メモリ４内に蓄積されている、第１５図のブロック
ＢｌｌのＢＳＴＤ部分■部分口ックＢ１２のＢＳＴＤ部
分■部分例して、ブロックＢＯＩのＢＳＴＤが作成され
る。その結果は第１３図（３）のＢＳＴＤ部分■部分酸
通シである。このＢＳＴＤ部分■部分酸においてレベル
０の受信＋Ｘが実行可能であると判定される。従って、
レベル１のブロックＢｌｒのＢＳＴＤ部分■部分口に、
実行可能であることを示すマークが付加され、このよう
に更新されたブロックＢｌｌのＢＳＴＤ部分■部分口リ
１に出力される。

また、レジスタ５内のレベル０に相当するフラグをセッ
トする。

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

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

回路ブロック１２の動作は既に説明した通シであシ、第
２，４図の例では、今回はレベル１のブロックＢｌｌの
ＢＳＴＤが更新され、第１３図（１）のＢＳＴＤ部分■
部分酸される。

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

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

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

以上の実施例では、各レベルのブロックのブロック状態
遷移図の作成には第２．３図を用いて説明した従来方式
を応用したが、他り方式を応用することも可能である。

例えば”グローバル状態遷移一括処理方式″（特願昭５
９−１９２４９１（昭和５９年９月１７日））”プロセ
ス別状態遷移展開法”（特願昭５９−２７１９３８（昭
和５９年１２月２５印）を応用することもできる。

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

【図面の簡単な説明】

第１図は本発明の実施例を示すブロック図、第２図は検
証対象プロトコル、第５図はグローバル遷移図、第４図
と第５図はプロトコル仕様の分割例を示す図、第６図は
圧縮処理を示す図、第７図は本発明の動作を示すフロー
チャート、第８図は第２図のプロトコル仕様のメモリ１
への蓄積形式の例を示す図、第９図と第１０図は各プロ
トコル仕様分割例及びその最大レベル値Ｌｍをメモリ２
゜に蓄積する形式例、第１１図はＢＳＴＤの蓄積形式例
、第１２図は第２図のプロトコル例を第１図の実施例に
適用して得られる各ＢＳＴＤを示す図である。 特許出願人　国際電信電話株式会社 特許出願代理人　弁理士山本恵　− 第２図 第４図 （ａ） Ｒｎ＋ 第３図 −−−−（貧打可能）宋定ｌ！１文信 第８図 第９図 第１０図 第１１図

Claims (1)

【特許請求の範囲】
1. 電気的信号により表現されたプロトコル仕様を入力とし
   て、該プロトコル仕様の有する論理誤りを検出・出力す
   るプロトコル検証方式において、前記プロトコル仕様を
   プロセスを単位として階層的に複数のブロックに分割し
   、各ブロックについて該ブロックに含まれるプロセス毎
   の状態と該プロセス間の信号受信バッファ内の信号系列
   とから構成されるブロック状態を生成し、該ブロック状
   態で実行可能なブロック遷移に従ってブロック状態を遷
   移しつつプロトコル仕様を検証することを特徴とするプ
   ロトコルの分割検証方式。