JPH0458743B2 - - Google Patents

Description

【発明の詳細な説明】 （産業上の利用分野） 本発明は、通信プロトコルの仕様を入力し、そ
れに含まれる内部矛循を仕様誤りとして検出し出
力するプロトコル検証方式に関する。 （従来技術） 近年の電気通信の高度化・多様化に伴い、交換
機・通信処理装置等の通信機器におけるソフトウ
エアは大規模化・複雑化する一方である。このた
め通信ソフトウエアの開発・保守における生産性
を向上させることは益々重要となつてきた。 通信ソフトウエアの開発・保守における生産性
を向上させる一つの有力な方策は、通信ソフトウ
エアの要求仕様を開発・保守の早い段階で正確に
かつ過不足なく定義することにより、それ以後の
段階からフイードバツク的な作業をなくすことで
ある。通信ソフトウエアの中で重要な位置を占め
るものとして、通信回線を介して各種の信号を送
受するための信号形式や手順を規定するプロトコ
ルがある。従つて、プロトコルの仕様に論理的矛
循やあいまいさがあつた場合、これを自動的に検
出するプロトコル検証技術が重要となる。 従来、この種のプロトコル検証方式としては、
与えられた通信プロトコル仕様に従つて、通信シ
ステムがとり得る動作および状態のすべての組合
せを順次列挙し、検査するものであつた。 この従来技術を第２図，第３図を用いて説明す
る。 第２図は、検証しようとするプロトコルの一例
であつて、プロセス１，２および３からなる通信
システムのプロトコル仕様を図示したものであ
る。ここで、通信システムとは、例えばプロセス
１および３が端末装置、プロセス３が交換機であ
るシステムであつてもよいし、また、プロセス
１，２，３がともにCPU内にあつてもよい。す
なわち、他の機能と信号の送受信（送信または受
信だけであつてもよい）を行う処理単位をプロセ
スと呼び、互いに信号の受授を行う複数のプロセ
スを総称して通信システムと呼ぶ。第２図はプロ
セス数３の場合のプロトコルの一例である。 第２図において、〇印は状態を、矢印は遷移を
表わす。また矢印に付けられたラベルは信号の送
信又は受信を示し、一般に−aⁱ _jはプロセスｉから
プロセスｊへの信号ａの送信を、＋aⁱ _jはプロセス
ｉから送信された信号ａのプロセスｊによる受信
を表わす。従つて、プロセス１はA₁を初期状態
として、プロセス２に対し信号１を送信して状態
B₁に遷移し、プロセス２から信号２を受信した
とき状態C₁に遷移し、プロセス３に対して信号
３を送信して初期状態A₁に戻るように動作する
ことが分かる。このように、各プロセスの動作は
比較的容易に理解できるが、プロセス１，２，３
の相互間に論理矛循があるか否かを判定すること
は容易でない。 前述したプロトコル検証の従来技術とは、一つ
の信号の送信又は受信による実行可能な遷移を初
期状態から遂一すべて順次に実行して、到達可能
な状態を全て含むような通信システム全体の状態
遷移図を作成し、その作成過程で論理矛循、すな
わち仕様誤りを検出していた。第２図のプロトコ
ル例に、この従来技術を適用した結果を第３図に
示す。この第３図はシステム全体の状態遷移を示
すことからグローバル遷移図と呼ぶ。また、状態
は、 印の中に各プロセスの状態が表示され、
これをグローバル状態と呼ぶ。 先ず、初期グローバル状態（A₁，A₂，A₃）に
おいて、定義されているプロセス遷移のうち、プ
ロセス１の−1¹ ₂とプロセス２における−2² ₁は全て
送信であり実行可能である。プロセス３において
定義されている遷移は全て受信であり、かつそれ
らの受信で受けるべき信号３もしくは信号４はい
ずれのプロセスからも送信されていないのでこれ
らの受信遷移は実行不可能である。つまり初期グ
ローバル状態（A₁，A₂，A₃）における実行可能
な遷移は−1¹ ₂と−2² ₁とが検出できる。そこで、先
ず−1¹ ₂の遷移についてテストし実行するとグロー
バル状態（B₁，A₂，A₃）となる。この状態で再
度実行可能な遷移を検出すると、＋1¹ ₂と−1² ₁とで
ある。このうち−1¹ ₂についてテストするとグロー
バル状態（B₁，C₂，A₃）となる。この状態から
即実行可能な遷移は−4² ₃だけでありグローバル状
態（B₁，B₂，A₃）となる。次にプロセス３が信
号４を受信しグローバル状態は（B₁，B₂，C₃）
となる。しかしながら、この状態においては、実
行可能な遷移はない。すなわち、プロセス１の状
態（B₁）においては信号２の受信がとり得る遷
移であるが、この状態前に信号２はプロセス２か
ら送信されていないので実行は不可能であり、ま
た、プロセス２の状態（B₂）においては、信号
１の受信が可能であるものの、プロセス１から送
信された信号１はすでにグローバル状態（B₁，
A₂，A₃）から（B₁，C₂，A₃）への遷移の過程で
処理されているし、さらにプロセス３の状態
（C₃）においては、信号５の受信が可能なもの
の、グローバル状態（B₁，B₂，C₃）となる以前
にいずれのプロセスからも信号５は送信されてい
ないので、これも実行不可能である。このよう
に、グローバル状態（B₁，B₂，C₃）においては
実行可能な遷移を全く持たない。このような状態
をデツドロツク状態といい、この状態を検出する
ことがプロトコル検証の１つの目的である。 また、第３図は、システムの実行可能な全ての
遷移を全て実行した結果であるから、第３図に含
まれない第２図の遷移は過剰であるといえる。こ
の観点からプロセス３の状態（C₃）における信
号受信＋5¹ ₃が過剰な定義として検出される。 さらに、第３図において、グローバル状態
（A₁，B₂，A₃）における実行可能な遷移は−1¹ ₂だ
けとなつているが、この状態になる前に信号２が
プロセス２からプロセス１に対して送信されてい
る。従つて、グローバル状態（A₁，B₂，A₃）に
おいて、信号２の受信遷移＋2² ₁が可能なはずであ
る。この遷移は、第２図のプロトコルに不足して
いる定義であり、未定義受信として検出される。
同様な意味で、グローバル遷移（A₁，B₂，D₃）
において、＋6³ ₂の未定義受信が検出される。 以上のように、初期グローバル状態（A₁，A₂，
A₃）から実行可能な遷移を遂一すべて順次に実
行することによりプロトコルの検証が行われる。 （発明が解決しようとする問題点） 上述した従来技術によつては、全ての実行可能
な遷移を検査の対象とするため、プロトコルが大
規模化・複雑化した場合、状態数や遷移数が膨大
となり、処理量すなわち処理時間の増大となり実
質的に検証が不可能となつていた。またハード化
の点からは、グローバル状態遷移図を記憶するた
めなどの膨大なメモリが必要となり、今だハード
の実現をみていない。 （問題点を解決するための手段） 本発明は、上述した従来技術の欠点に鑑みなさ
れたもので、処理量の少ないプロトコル検証方式
を提供することを目的とし、その特徴は、仕様誤
りを検出するのに支障ない範囲で通信システムの
動作を一括し、必要最小限の状態と動作を列挙し
て検査することにある。 （作用） 本発明によつては、(1)直ちに実行できる遷移の
組合せによるグローバル遷移候補を導出し、(2)冗
長なグローバル遷移候補を削除し、(3)送受信遷移
一括処理によるグローバル遷移を最終決定するこ
とにより、検査の対象となる遷移数のグローバル
状態数を削減するので、ハードの量及び処理時間
が減少し発明の目的を達成することができる。 （実施例） 本実施例が検証の対象とするプロトコルは、従
来技術と同様第２図に示したプロトコルの例とす
る。 ここで、プロトコル仕様と仮定および説明のた
めの用語について整理しておく。 本実施例では、検証対象とするプロトコルの仕
様は、以下に示すQ_i，O_i，M_ij，succ（ij＝１，…，
Ｎ；Ｎ：プロセスの個数）の４項の組み合せで与
えられるものとする。 Q_i：プロセスｉの状態集合。 O_i：プロセスｉの初期状態。 M_ij：プロセスｉからプロセスｊに送る信号の
集合。ただしM_ii＝Φ（空集合）（ｉ＝
１，…，Ｎ）とする。 succ：プロセスが各状態で信号を送受信するこ
とにより遷移した結果とる状態を表わ
す関数で、succ（ｓ，ｘ）は、、状態ｓ
にあるプロセスが信号ｘの送信（ｘ＜
０）又は受信（ｘ＞０）により遷移し
た後の状態を表わす。 また、検証対象とするプロトコルに対し、以下
の仮定を設ける。 信号の送受により各プロセスが遷移する先の
状態は、その信号の元の状態に応じて一意に定
まる。 一旦初期状態を遷移した後再び初期状態に戻
つた場合にはそれ以上遷移しないものとする。 各プロセスは、容量が十分大きな信号受信用
バツフアを相手プロセス別に持つ。 プロセス相互間で送受する信号の受信順序は
送信順序と同一である。 以上の仮定の内は、実施例の説明を単純にす
るためのものであり、省略することも可能であ
る。 次に、実施例により検出する仕様誤りを明らか
にするが、その前に準備として、いくつかの用語
を定義する。 プロトコルを用いて通信するシステム全体の状
態ＧをＳとＣの２項の組み合せ、即ちＧ＝＜Ｓ，
Ｃ＞で定義し、Ｇをグローバル状態と呼ぶ。ここ
で、Ｓ＝（s₁，…s_N，Ｃ＝（c₁₁，c₁₂，…，c_NN）で
あり、s_iはプロセスｉの状態、c_ijはプロセスｉか
らプロセスｊに送出されたが未が受信処理されて
いない信号受信バツフア上の信号の系列である。
信号受信バツフアがすべて空のグローバル状態Ｇ
＝＜Ｓ，＜ε＞ij^N＝１＞安定グローバル状態と呼
ぶ。特に各プロセスの初期状態を含む安定グロー バル状態Ｇ＝＜ _i>ｉＮ ＝ １，<ε>ｉ，j^N１＞ を初期グローバル状態と呼びG₀で表わす。尚、
誤解することがない場合には、グローバル状態を
個々のプロセスの状態のみで表わすこともある。 グローバル状態Ｇにおいて、一つの信号を送信
或は受信することによりのグローバル状態G′に
遷移するときＧとG′の関係をＧ⊥G′で表わす。
更に、初期グローバル状態G₀からこのような遷
移をくり返すことにより到達するＧ、即ちG₀⊥
…⊥ＧであるＧは到達可能であるという。 あるプロセスの状態ｓと信号ｘより成る順序対
＜ｓ，ｘ＞を、ｘ＜０であれば信号送信遷移、ｘ
＞０であれば信号受信遷移と呼ぶ。与えられたプ
ロトコル仕様にsucc＜ｓ，ｃ＞が定義されている
とき、＜ｓ，ｘ＞を定義済遷移又は定義済送／受
信と呼ぶ。 定義済送信＜ｓ，ｘ＞（ｘ＜０）は、ｓを要素
として含む到達可能なグローバル状態が存在する
とき実行可能である。また定義済受信＜ｓ，ｘ＞
（ｘ＞０）は、ｓを要素として含みかつ該当する
信号受信バツフアの先頭に信号ｘを蓄積している
到達可能グローバル状態が存在するとき実行可能
である。 グローバル状態Ｇから別のグローバル状態
G′に移る遷移をグローバル遷移と呼び｛ ｝印
で表わす。 以上の準備に基づいて、本発明が検出するプロ
トコル仕様の誤りを示すと以下の通りである。 信号定義の過剰：プロトコル仕様に含まれる
信号の送受信の内実行し得ないもの。 信号定義の不足：プロトコル仕様に含まれな
いが実行可能である未定義受信。 デツドロツク状態：すべてのプロセスについ
て状態遷移が実行不可能であり、かつすべての
信号受信バツフアが空である安定グローバル状
態。 第１図は、本発明の一実施例を示すブロツク図
である。第１図で、１は外部から与えられるプロ
トコル仕様を蓄積するメモリ、２は検証処理に使
用する各種変数の初期値を設定する初期設定ブロ
ツク、３は指定されたグローバル状態における実
行可能な未定義受信を検出する未定義受信検出ブ
ロツク、４は指定されたグローバル状態において
直ちに実行可能な遷移を抽出する実行可能遷移抽
出ブロツク、５は指定されたグローバル状態にお
けるグローバル遷移の候補を導出するグローバル
遷移候補決定ブロツク、６はグローバル遷移候補
決定ブロツク５の処理結果を入力し、冗長なグロ
ーバル遷移候補を除去する冗長グローバル遷移候
補削除ブロツク、７は冗長グローバル遷移候補削
除ブロツク６の処理結果に対して送信遷移と受信
遷移を可能な範囲で一括処理することによりグロ
ーバル遷移を最終決定する送受信一括ブロツク、
８は送受信一括ブロツク７で得られたグローバル
遷移、およびそれらを実行して得られるグローバ
ル状態の内、その時点までに得られているグロー
バル状態遷移図（これは後述のメモリ１２に蓄え
られている）に含まれないものを追加することに
よりグローバル状態遷移図を更新するグローバル
状態遷移図更新ブロツク、９はブロツク８で更新
されたグローバル状態遷移図から未処理グローバ
ル状態を検索し、未処理グローバル状態が検出で
きたときはその一つを後述のメモリ１２に出力
し、それや検出できなかつたときはその旨の情報
を次に示す実行不可能送受信検出ブロツクへ出力
する未処理グローバル状態抽出ブロツク、１０は
プロトコル仕様に含まれる信号の送受信とグロー
バル状態遷移図に含まれる信号の送受信とを比較
し、実行不可能な定義済送受信を求める実行不可
能送受信検出ブロツク、１１は指定されたグロー
バル状態がデツドロツクであるか否か判定するデ
ツドロツク検出ブロツク、１２は検証結果である
グローバル状態遷移図等および各種の変数を蓄積
するメモリである。 第４図は、プロトコル仕様をメモリ１に蓄積す
る場合の一蓄積形式を、第２図のプロトコル例に
ついて示す。第４図で、プロセス名欄、状態名、
遷移の各欄は、それぞれプロセスの名称（第２図
の例では１〜３）、対応するプロセスが持つ状態
の名称、対応するプロセス状態が持つ遷移（遷移
に伴つて送受信する信号名を表わすラベルと、遷
移後の状態名から構成される）を表わす。また第
５図は、本発明により出力されるグローバル状態
遷移図及び仕様誤りを表形式でメモリ１２に蓄積
する場合の一蓄積形式を後述の第６図の例につい
て示す。第５図ａはグローバル状態遷移図の一蓄
積形式でグローバル状態名とグローバル遷移の各
欄はそれぞれグローバル状態の名称と、対応する
グローバル状態が持つグローバル遷移（遷移に伴
つて送受信する信号名を表わすラベルと、遷移後
のグローバル状態の名称とから構成される）を表
わす。第５図ｂは未定義受信の一蓄積形式でプロ
セス名、グローバル状態、未定義受信ラベルの各
欄は、それぞれ未定義受信を持つプロセスの名
称、未定義受信を持つグローバル状態（プロセス
の状態と、プロセス間信号受信バツフア内信号の
系列とから構成される）を表わす。第５図ｃはデ
ツドロツクとなるグローバル状態を、第５図ｂの
グローバル欄と同様な方法で表わす。第５図(d)は
実行不可能送受信の一蓄積形式で、プロセス名、
状態名、遷移ラベルの各欄はそれぞれ実行不可能
送受信を持つプロセスの名称、実行不可能送受信
が定義されているプロセス状態の名称、実行不可
能送受信遷移を表わす。 第６図は、第２図のプロトコル例を第１図の実
施例に適用した結果得られるグローバル状態遷移
図を示す。以下、第２，６図の例を用いて、第１
図の実施例の動作を説明するが、プロトコル仕様
は第４図の形式で既にメモリ１で蓄えられている
ものとする。第１図のブロツク図では、最初に初
期設定ブロツク２が動作する。初期設定ブロツク
２はメモリ１にアクセスし、プロトコル仕様に含
まれる各プロセスの初期状態を入力して初期グロ
ーバル状態を求め、以後の各ブロツクにおいて検
証処理の対象とするグローバル状態を指定する変
数Ｇに初期グローバル状態を設定する。さらに、
未処理グローバル状態の集合を表わす変数〓を空
集合に設定する。これらの情報をメモリ１２に出
力して蓄積し、未定義受信検出ブロツク３を起動
する。 第７図は未定義受信検出ブロツク３の動作を示
すフローチヤートである。 未定義受信検出ブロツク３は、まずメモリ１２
にアクセスし、変数Ｇの値を入力する。次にメモ
リ１のプロトコル仕様情報を用いて、Ｇの示すグ
ローバル状態において実行可能でかつ未定義の受
信を、以下の方法により検出する。即ち、 グローバル状態Ｇにおける信号受信バツフア
の内、空でないものについて、その先頭にある
信号の受信がプロトコル仕様に定義されている
か否かを調べる。そして定義されていない受信
をすべて実行可能未定義受信とし、その情報を
メモリ１２に出力する。 グローバル状態Ｇにおける空の信号受信バツ
フアの各々について次の処理を行う。その信号
受信バツフアが蓄えるべき信号の送信プロセス
をｉ、受信プロセスをｊとする。プロセスｉが
グローバル状態Ｇにおいてプロセスｊ宛の送信
遷移を持つか否か検査し、送信遷移を持つ場合
にはそのような送信遷移によつて送出される信
号を受信する受信遷移をプロセスｉがグローバ
ル状態Ｇで持つか否か調べる。そして、そのよ
うな受信遷移をプロセスｉが持たないとき、そ
れを実行可能未定義受信とし、その情報をメモ
リ１２に出力する。 例えば第２，６図の初期グローバル状態（A₁，
A₂，A₃）においては、信号受信バツフアはすべ
て空である。そしてこのグローバル状態では、送
信遷移として−1¹ ₂，と−2² ₁が定義されている。こ
の内、−2² ₁に対応する受信遷移はこのグローバル
状態では定義されていない。従つて、実行可能未
定義受信として＋2² ₁が出力される。 未定義受信検出ブロツク３は、以上の動作を終
えると、実行可能遷移検出ブロツク４を起動す
る。 実行可能遷移検出ブロツク４は、メモリ１と１
２にアクセスし、以下のとに示す方法で、グ
ローバル状態Ｇにおいて直ちに実行可能な送受信
遷移を抽出しその結果をグローバル遷移候補決定
ブロツク５に出力する。 グローバル状態Ｇで定義されている送信はす
べて直ちに実行可能であると判定する。例え
ば、第１図のプロトコル例で初期グローバル状
態（A₁，A₂，A₃）において、−1¹ ₂および−2² ₁は
それぞれプロセス１，２が直ちに実行可能な送
信遷移である。 グローバル状態Ｇで定義されている受信の
内、それに対応する信号受信バツフアが、その
受信遷移の指定する信号をその先頭に含んでい
るものをすべて直ちに実行可能であるとする。
例えば、第１図のプロトコル例において、初期
グローバル状態でプロセス遷移−1¹ ₂と−2² ₁を実
行して得られるグローバル状態（B₁，B₂，A₃）
では、信号受信バツフアC₁₂，C₂₁の内容はそれ
ぞれC₁₂＝〔１〕、C₂₁＝〔２〕であるので、プロ
セス１，２で定義されている受信遷移＋1¹ ₂と＋
2² ₁はともに直ちに実行可能である。 ブロツク４は、以上の処理を終えるとグローバ
ル遷移候補決定ブロツク５を起動する。なお直ち
に実行可能な遷移がないときはブロツク１１を起
動する。 グローバル遷移候補決定ブロツク５は、実行可
能遷移検出ブロツク４での処理結果を入力し、以
下の処理によりグローバル遷移候補を決定した
後、その結果を冗長グローバル遷移候補削除ブロ
ツク６に出力し、ブロツク６を起動する。 一つのグローバル状態において、直ちに実行可
能なプロセス遷移が１個であれば、そのグローバ
ル状態からのグローバル遷移候補はそのプロセス
遷移とする。直ちに実行可能なプロセス遷移が複
数個ある場合は、直ちに実行可能なプロセス遷移
の組合せの内、各プロセスで実行する遷移が高々
１個であるような組合せすべてを、そのグローバ
ル状態からのグローバル遷移候補とする。 このようにして求められるグローバル遷移候補
には、直ちに実行可能な遷移を持つプロセスの遷
移を含まないものもある。このようなグローバル
遷移候補を実行して得られるグローバル状態以降
では、元のグローバル状態でそのようなプロセス
が直ちに実行可能だつた遷移を除外してグローバ
ル遷移候補を求める。 例えば第２図のプロトコル例で、初期グローバ
ル状態（A₁，A₂，A₃）において直ちに実行可能
な遷移は、プロセス１での−1¹ ₂およびプロセス２
での−2² ₁である。これらの組合せによるグローバ
ル遷移候補は、｛−1¹ ₂｝，｛−2² ₁｝，｛−1¹ ₂，−2² ₁
｝の
３通りある。これらの３つのグローバル遷移候補
の内、｛−2² ₁｝は、次に述べる冗長グローバル遷
移候補の削除処理により除去され、最終的には第
２図に示す通り｛−1¹ ₂｝と｛−1¹ ₂，−2² ₁｝の２通
りとなり、各々を実行すると、新グローバル状態
として（B₁，A₂，A₃）と（B₁，B₂，A₃）が得
られる。 初期グローバル状態（A₁，A₂，A₃）からグロ
ーバル状態（B₁，A₂，A₃）へのグローバル遷移
｛−1¹ ₂｝は、初期グローバル状態で直ちに実行可
能な遷移−2² ₁を持つプロセス２の遷移を含まな
い。従つて、グローバル状態（B₁，A₂，A₃）か
らのグローバル遷移を求める場合には、プロセス
２の遷移−2² ₁が除外され、その結果、グローバル
状態（B₁，A₂，A₃）からのグローバル遷移は、
第３図に示すように｛＋1¹ ₂｝のみとなる。 以上の動作を終えると、ブロツク５はブロツク
６を起動する。 冗長グローバル遷移候補削除ブロツク６は、ブ
ロツク５のグローバル遷移候補決定処理により得
られるグローバル遷移候補の内、次に示す二つの
条件ａ，ｂを満たすプロセスの遷移を含まないよ
うな組合せのグローバル遷移を削除し、その結果
を送受信一括ブロツク７へ出力し、ブロツク７を
起動する。 ａ そのプロセスのその状態における定義済遷移
がいずれも直ちに実行できる遷移か実行し得な
い受信遷移のいずれかであり、かつ直ちに実行
可能な遷移が１個以上存在すること。ここで、
グローバル状態Ｇで定義された受信は、それ
を直ちに実行することができない。かつそれに
対応する送信がグローバル状態Ｇ以降に定義さ
れていない、即ちＧから初期状態まで各プロセ
スの定義済遷移をその遷移方向にたどつていつ
たときそのような信号が存在しない場合、およ
び、該当する受信バツフアに別の信号が存在
する場合、実行し得ないと判定する。 ｂ そのプロセスはその状態で他プロセスから信
号を受信することがない。或は受信することが
可能でかつその最初の信号が特定できること。
ここで、あるプロセスに対する送信がグローバ
ル状態Ｇ以降全く定義されていない場合、その
プロセスはその状態で他プロセスから信号を受
信し得ないと判定する。また、あるグローバル 状態Ｇ＝＜ｉＮ ＝ １，ｉ，j^N=１＞ においてプロセスｋが状態s_kでプロセスｉから最
初に受信する信号を特定できるための条件は、
グローバル状態Ｇにおけるプロセスｉのすべての
定義済遷移がプロセスｋへの送信か又は実行不可
能である、プロセスｉからプロセスｋ宛の受信
バツフアが空でない、のいずれかが成立すること
である。 例えば、第２，６図の例で、初期グローバル状
態（A₁，A₂，A₃）からのグローバル遷移候補は
｛−1¹ ₂｝，｛−2² ₁｝，｛−1¹ ₂，−2² ₁｝の３通りであ
つ
た。そして、次に示すように、初期グローバル状
態（A₁，A₂，A₃）においてプロセス１は上記の
２条件ａ，ｂを満たすので、３つのグローバル遷
移候補の内、プロセス１の遷移を含まないグロー
バル遷移候補｛−2² ₁｝を冗長なものとして削除す
ることができる。実際、プロセス１の状態A₁に
おける定義済遷移は−1¹ ₂のみであり、これは直ち
に実行可能である。従つて、プロセス１は条件ａ
を満たす。一方、プロセス２からプロセス１へ送
る信号は２のみであり、かつプロセス２は状態
A₂で信号２をプロセス１に送出することができ
る。従つて、プロセス１が状態A₁でプロセス２
から最初に受信する信号は、２と特定できる。ま
た、プロセス３はプロセス１に対して送出する信
号を持たない。従つて、プロセス１は状態A₁で
プロセス３から信号を受信することがない。つま
り、プロセス１は条件ｂを満たす。 送受信一括ブロツク７は、冗長グローバル遷移
候補削除ブロツク６での処理の結果得られるグロ
ーバル状態Ｇからのグローバル遷移候補の内、送
信遷移を含むものについて、 ａ その送信に対応する受信が元のグローバル状
態Ｇで定義されており、かつその受信バツフア
が空であること。 ｂ その受信プロセスはその状態で他に定義済遷
移を持たない、或は他に定義済遷移を持つ場合
それらはすべて実行し得ない受信であること。 ｃ その受信プロセスは、その信号を送るプロセ
ス以外の各プロセスからその状態で信号を受信
することがない、或は受信することが可能でか
つその最初の信号が特定できること。 の３条件が成立する場合、そのような信号受信遷
移をそのグローバル遷移に含め、これらを統合し
て一つのグローバル遷移とする。このような処理
を送受信遷移一括処理と呼び、その結果を、グロ
ーバル状態遷移図更新ブロツク８へ出力する。 例えば第２，６図の例で、ブロツク４〜６の処
理により、安定グローバル状態（A₁，D₂，B₃）
におけるグローバル遷移は、｛−6³ ₂｝のみとなる。
ところが、この信号を受信するプロセス２は、こ
れを受信する遷移＋6³ ₂以外実行できる遷移を持た
ないので上記の条件ａ，ｂを満たす。更にプロセ
ス２が状態D₂でプロセス１から信号を受けるこ
とがなく、またプロセス３から最初に受ける信号
は６と特定のできる条件ｃを満たす。従つて、グ
ローバル状態（A₁，D₂，B₃）からのグローバル
遷移｛−6³ ₂｝は、プロセス２の受信遷移＋6³ ₂を統
合した｛±6³ ₂｝となる。 ブロツク７は以上の動作を終えると、ブロツク
８を起動する。 グローバル状態遷移図更新ブロツク８は、送受
信一括ブロツク７で最終決定したグローバル遷移
に関する情報を入力し、それに基づいてメモリ１
２内のグローバル状態遷移図および未処理グロー
バル状態集合〓を更新する。具体的には、まず、
メモリ１内のプロトコル仕様を用いて、ブロツク
７から得られる各グローバル遷移を実行した結果
得られる新しいグローバル状態を決定する。次
に、以上で得られたグローバル遷移および未処理
グローバル状態をメモリ１２のグローバル状態遷
移図に追加する。さらに、以上で得られたグロー
バル状態のうち、メモリ１２内のグローバル状態
遷移図に含まれるグローバル状態と同一のものを
除き、メモリ１２内の未処理グローバル状態の集
合〓に追加し、ブロツク９を起動する。 未処理グローバル状態抽出ブロツク９は、メモ
リ１２上の〓にアクセスし、その中から一つの未処
理グローバル状態を検索する。もし未処理グロー
バル状態が存在しないときは、実行不可能送受信
検出ブロツク１０を起動する。未処理グローバル状
態が存在するときは、メモリ１２内のＧにそれを
蓄積し、未定義受信検出ブロツク３を起動する。 実行不可能送受信検出ブロツク１０は、メモリ
１内のプロトコル仕様に含まれる送受信遷移と、
メモリ１２内のグローバル状態遷移図に含まれる
送受信遷移とを比較し、前者に含まれるが後者に
含まれない送受信遷移を実行不可能送受信として
メモリ１２に出力する。 デツドロツク検出ブロツク１１は、メモリ１内
のプロトコル仕様を参照して、メモリ１２内のＧ
で指定されたグローバル状態において直ちに実行
可能な遷移が存在するか否かを調べる。その結果
が否のときのみ、そのグローバル状態をデツドロ
ツクとしてメモリ１２に蓄積する。その後、未処
理グローバル状態抽出ブロツク９を起動する。 以上述べた方法により、仕様誤りをすべて正し
く検出できる。その理由を以下に説明する。既に
述べたように、本発明による方式が従来方式と異
なるのは、即時実行可能遷移抽出ブロツク４〜送
受信一括ブロツク７の動作にあるので、これらの
ブロツクの動作によつて仕様誤りを検出し損なう
ことがないことを説明する。尚、以下では、ブロ
ツク４と５の処理をまとめて第１の処理、または
ブロツク６と７の処理をそれぞれ第２，第３の処
理と呼ぶ。 まず、第２，第３の処理を実行せず、第１の処
理結果を直接ブロツク８に出力することによつて
仕様誤りを検出し損なうことがないこと、即ち、
第１の処理により得られるグローバル遷移をすべ
て実行してグローバル状態遷移図を作成すること
により、先述した仕様誤りをすべて検出できるこ
とを説明する。 第１の処理は、実行可能となつたプロセス遷移
の各々について、実際に実行する場合と実行しな
い場合とに明確に分け、前者の場合には実行する
遷移をすべて直ちに実行させてしまうものであ
る。従つて、検出不可能となる実行可能な定義済
送受信がないことは明らかである。一方、一般
に、あるグローバル状態に到達するための実行プ
ロセス遷移系列において実行するプロセス遷移の
順序を入れ替えた場合、入れ替え後の系列が実行
可能でかつ各プロセス毎の系列の順序が変らない
ならば、到達するグローバル状態は変わらない。
言い換えると、第１の処理によりすべての到達可
能なグローバル状態を列挙できる。従つて、検出
不可能となる実行可能な未定義受信やデツドロツ
ク状態はない。 以上で第１の処理、即ちグローバル遷移候補決
定処理のみによつてグローバル状態遷移図を作成
することにより仕様誤りをすべて検出できること
が言える。 次に、第１の処理、即ちグローバル遷移候補導
出処理の結果に第２の処理、即ち冗長グローバル
遷移候補の削除処理を加えて得られるグローバル
遷移を用いてグローバル状態遷移図を作成するこ
とにより、仕様誤りをすべて検出することができ
ることを説明する。 冗長グローバル遷移候補削除処理により実行可
能な定義済遷移が実行不可能となることはないの
で、実行可能な定義済遷移を検出し損なうことが
ないのは明らかである。一般にあるグローバル状 態Ｇ＝＜ｉＮ ＝ １，ｉ，j^N＝１＞にお いて、プロセスｋの遷移を含まないグローバル遷
移を除外すると、プロセスｋの状態s_kで実行可能
な未定義受信を検出し損なうことがある。しかし
この処理では、先に述べた条件ｂが成立するプロ
セス、即ち他プロセスから最初に受信できる信号
が特定できるプロセスについてのみそのようなグ
ローバル遷移を除外するので、実行可能な未定義
受信を検出し損なうことはない。 また、一般に冗長グローバル遷移候補削除処理
により（安定）グローバル状態が一部削除され
る。しかし削除されたグローバル状態は、元のグ
ローバル状態Ｇからのグローバル遷移を実行した
結果得られる新しいグローバル状態のいずれかと
元のグローバル状態Ｇとの途中に位置し、必ず前
者のグローバル状態に遷移することが可能であ
り、デツドロツクとはならない。従つてデツドロ
ツク状態を検出し損ねることはない。 以上から、第１の処理に第２の処理を追加して
グローバル状態遷移図を作成することにより、仕
様誤りをすべて検出できることが言える。 次に、第３の処理、即ち送受信一括処理を第
１，第２の処理に追加して得られるグローバル状
態遷移図を作成することにより、仕様誤りをすべ
て検出できることを説明する。この第３の処理は
単に実行可能な受信処理を早く行うものであり、
他の実行可能な遷移の実行を妨げることはない。
従つて、実行可能な定義済遷移を検出し損なうこ
とがないのは明らかである。また先に述べた条件
ｃから、一括処理される受信を持つプロセスのそ
の状態で実行可能な受信は漏れなく検出できるの
で、実行可能な未定義受信を検出し損なうことは
ない。さらにこの第３の処理は受信のみを早く実
行するので、この処理により安定グローバル状態
が除去されることはない。従つて、デツドロツク
状態を検出し損なうことはない。 以上から、第１，２および第３の処理をすべて
実行してグローバル状態遷移図を作成することに
より、プロトコル仕様に含まれる誤りをすべて検
出できることが分かる。 （発明の効果） 以上詳細に説明したように、本出願による方式
は、従来方式に比較すると仕様誤りの検出に支障
ない範囲で各プロセス３の遷移を一括してグロー
バル状態遷移図を作成する。このため、従来方式
に比較するとグローバル状態遷移図に含まれるグ
ローバル状態およびグローバル遷移とも大幅に減
少する。例えば、第２図のプロトコル例に対する
それらの値の比較を第８図に示す。このため、従
来方式に比較して、本出願による方式は検証処理
に必要となる処理量が大幅に減少するとともに、
グローバル状態遷移図等を蓄積するために必要と
なるメモリの容量を大幅に削減することができる
という利点がある。

【図面の簡単な説明】

第１図は本発明の一実施例を示すブロツク図、
第２図と第３図はプロトコル検証の説明図、第４
図はプロトコル仕様のメモリへの蓄積を示す例、
第５図ａ〜ｄはグローバル状態遷移及び仕様誤り
をメモリに蓄積する例を示す図、第６図は第２図
のプロトコル例を第１図に適用して得られるグロ
ーバル状態遷移図、第７図は未定義受信検出ブロ
ツクの動作を示すフローチヤート図、第８図は第
２図のプロトコル例に対する遷移数と状態数を従
来の技術と本発明について示す図である。

Claims (1)

1. 【特許請求の範囲】 １ 通信システムにおける送受信の信号形式や手
   順を規定するプロトコル仕様を入力として、該プ
   ロトコル仕様の有する遷移情報に従つてプロトコ
   ル動作を模擬することによりプロトコル仕様を検
   証するプロトコル検証回路において、 外部から与えられるプロトコル仕様を蓄積する
   第１のメモリと、 検証結果であるグローバル状態遷移図及び各種
   の予め設定された変数を蓄積する第２のメモリ
   と、 検証処理に使用する各種変数の初期値を設定す
   る変数初期値設定手段と、 システム内の各プロセスの状態を示し、かつ指
   定されたグローバル状態における実行可能な未定
   義受信を検出する未定義受信検出手段と、 指定されたグローバル状態において直ちに実行
   可能な遷移を抽出する実行可能遷移抽出手段と、 指定されたグローバル状態におけるグローバル
   状態の候補を導出するグローバル遷移候補決定手
   段と、 該グローバル遷移候補決定手段の処理結果を入
   力とし、冗長なグローバル遷移候補を除去する冗
   長グローバル遷移候補削除手段と、 該冗長グローバル遷移候補削除手段の処理結果
   に対して送信遷移と受信遷移を可能な範囲で一括
   処理することによりグローバル遷移を最終決定す
   る送受信一括手段と、 該送受信一括手段により得られたグローバル遷
   移、及び該グローバル遷移を実行して得られるグ
   ローバル状態の内、第２のメモリに蓄積されてい
   るグローバル状態遷移図に含まれないものを追加
   することによりグローバル状態遷移図を更新する
   グローバル状態遷移図更新手段と、 プロトコル仕様に含まれる信号の送受信とグロ
   ーバル状態遷移図に含まれる信号の送受信とを比
   較し、実行不可能な定義済送受信を求める実行不
   可能送受信検出手段と、 前記グローバル状態遷移図更新手段により更新
   されたグローバル状態遷移図から未処理グローバ
   ル状態を検索し、未処理グローバル状態が検出で
   きた時は当該検出した未処理グローバル状態を第
   ２のメモリに蓄積し、検出できなかつた時は当該
   検出不可の情報を前記実行不可能送受信検出手段
   へ出力する未処理グローバル状態抽出手段と、 指定されたグローバル状態において実行可能で
   ない遷移が存在しないときの当該グローバル状態
   をデツドロツクであるとし、デツドロツクである
   か否か判定するデツドロツク検出手段とからなる
   ことを特徴とするプロトコル検証回路。