| 研究概要 |
1.再送回数等をパラメータ化して扱うために, プロトコルマシンを, 非負整数を保持する有限個のレジスタから成るオートマトンとしてモデル化できるかどうかを検討した. そして, このモデルの枠組みの中で, BSC手順やHDLC手順等実用のプロトコルに基づくプロトコルマシンの仕様記述を行い, それらに対しては, このモデルでエラーリカバリ方法も含め, 仕様を記述できることを確かめた.
2.また, 1.で定義したオートマトンから成る通信系(ネットワーク)全体の動作並びにエラーリカバリ性を形式的に定義した. 例えば, 2局間通信の場合, 1.で検討した2つオートマトンの直積マシンが通信系全体を表すと定義し, 直積マシンの状態対を正常な状態対とエラーの状態対に分類し, エラーの状態からいつかは正常な状態対に到達とエラーの状態対に分類し, エラーの状態対からいつかは正常な状態対に到達できる時, 且つその時のみ, エラーリカバリ性をもつと定義した(2局間以外の場合も同様に定義する).
3.さらに, エラーリカバリ性をもつための一つの十分条件を与え, その十分条件が成り立つかどうかの判定問題を整数線形計画問題の解の非存在性の判定問題に帰着して判定する方法を考案した. 整数線形計画問題の解の非存在性判定プログラムは作成してある. 現在, HDL手順を例として, 実用規模のプロトコルに対してこの方法が適用可能かどうかについて検討を行なっている. 代数的手法及びテンポラルロジックを利用した記述・検証法についても検討を進めている.
4.エラーリカバリ性の定義及びエラーリカバリ性を持つための十分条件等については, 昭和63年電子情報通信学会春季全国大会で発表する. また3.の整数線形計画問題の解の非存在性判定に基づいてプロトコルマシンの互換性(等価性)を証明する方法についても検討し, その結果を電子情報通信学会論文誌(D)に投稿中である.
|
