計算機ネットワーク構成の設計、検証及び管理のための形式手法

1998 Fiscal Year Annual Research Report

• Project/Area Number: 10878048
• Research Institution: Nagasaki University
• Principal Investigator: 鶴 正人 長崎大学, 総合情報処理センター, 助手 (40231443)
• Keywords: ネットワーク / 形式手法 / 経路表 / 検証 / 書換え規則 / 属性文法

Research Abstract

1. 形式表現と性質の検証
ノード(エンドノード及びルータ)とサブネットワークをプロセスとし、その並列合成としてネットワーク全体をみて、単項π計算によって表現した。経路表はメッセージの宛先による和(選択)になり、代替経路も表現可能である(主経路のルータが利用不可であることをプロセス外からの通知によって知る必要がある)。このモデル化の上で抽象度の異なるネットワーク設計間の対応の検証(双模倣性等)や適切な様相論理を使ったイベント発生系列に関する性質の検証が可能になる。現在、その有効性/実用性を調べている。
2. 書換え規則による段階的なネットワーク構成/経路の設計
クライアント/サーバ型の利用を想定したネットワークにおいて、異なる種類/異なる場所のものを含むサーバ及びクライアント群が与えられた時に、特定の種類のクライアント/サーバ関係や場所ごとの必要条件を満す単純なネットワークから始めて、分散、ネットワーク2重化、ルータ2重化、マージなどの書換え(変形/合併)規則を使って、最終的に適切な全体ネットワーク(構成と経路)を導出することを試みている。現在、規則の厳密化や意味付け、書換え過程で保存できる性質(例えば、その経路がある動的経路制御プロトコルを用いた時の安定解になり得るか等)について調べている。
3. 定量的性質の計算
定量的性質(流量、遅延、通過禁止、帯域配分等)は、各宛先毎の経路木上の局所計算を繰り返し、最後に全宛先に関してマージすることで計算できる。そこで、属性文法を用いて各種属性を統一的に効率よく計算する手法、特に変更時のインクリメンタルな計算を検討している。ただし、宛先毎の経路木は(負荷分散経路を許す場合)必ずしも木にはならず、現在、属性文法の拡張(高階等)について調べている。