| 研究課題/領域番号 |
61460130
|
|---|
| 研究機関 | 東京大学 |
|---|
研究代表者 |
斉藤 忠夫 東大, 工学部, 助教授 (30010789)
|
|---|
| 研究分担者 |
富山 忠宏 東京大学, 工学部, 助手 (80010932)
相田 仁 東京大学, 工学部, 講師 (00175712)
|
|---|
| キーワード | 通信プロトコル / イベント順序表現 / 形式記述法 / 状態遷移図 / 検証 |
|---|
| 研究概要 |
通信プロトコルなコンピュータとコンピュータの間の対話のルールである。正常な通信のメッセージ形式と手順を規定するのみならず、両者の動作速度に不整合が生じたときの処置、通信に誤りが生じたときの処置、誤った手順が発生したときの処置、いずれかに通信上の不都合(バッファあふれなど)が生じたときの処置等を規定する。これらの多様な規定は通常自然言語で記述されるのが普通であるが、異る解釈が行なわれると接続が不可能になることがあり得る。
このためプロトコルには各種の形式的記述法が提案されており、これを使用したインプリメンテーション法と検証法が研究されている。特にイベント順序記述と状態遷移図が、それぞれ検証ルールの記述とインプリメンテーションのための記述として知られている。しかし従来この二つの記述法は独立したものとされており、この間の関係は充分に解明されていない。
本研究においては、プロトコル検証の立場から、人間の記述に近いイベント順序形の形式的記述法を、時間論理にもとずいて新たに規定し、これをインプリメントに適した状態遷移表記述に変化する方式を検討した。
イベント順序ルールによる記述はまず原始状態図に変換される。これは可能なすべてのイベントの並びを直接表現するものであり、記述の検証に適している。次に原始状態図の中から入力待ちの状態を検出して状態遷移表に変換する。これはインプリメントと製品検証に適している。
本年度においてはこのようなプロトコルの形式記述法を主としてデータリンク層のプロトコル記述に対して適用しその見通しを得た。同時に形式記述方式のプロトコル記述能力、記述の段階的詳細化、モジュール的な記述などについて多くの知見を得た。
|
