7.1
序 盲プログラムの正しさの形式的な検証は一般には困難な問題であり，大量の計 算時聞を要するなど，効果的な検証法はあまり開発されていない[九通信プロ
トコルの検証は，プログラムの規模が手頃であること，対象が限定されること，
並行処理を含む興味，等から比較的よく研究されている[九われわれは，実際 のプログラム例として主に通信プロトコルを取り上げ，代数的にその仕様を記 述するとともに，検証支援システムを用いてそれらの正しさの検証を行ってき た[1]‑[九本章では，第4章 第6章で記述・検証の対象となったポイント・
ツー・ポイント型のプロトコルよりも，分散処理志向がより強く規格の上で主 張されており，かつ，間接的ではあるがネットワーク全体の動作まで規定して いるプロトコルとして， ローカルエリアネットワーク
(LAN
，L o c a l Area Network)
プロトコルを取り上げる。具体的には， トークンリング方式LAN
プロトコルを対象とする。トークンリング方式
LAN
で、は，通信媒体を介して複数の局を環状に接続す るとし、う形態をとる。この環状に閉じた通信媒体をリングと呼び， リング上を 流れる情報の伝送単位をパケットと呼ぶ。局から送信されるパケットは， リン グ上をあらかじめ定められた一方向にのみ進む。パケットには フレーム"と トークン"の2
種類がある。フレームは発信局アドレス，着信局アドレスお よび発信局から着信局へ伝達されるべき可変長のデータを含み， トークンは発 信権受け渡しの制御に用いられる。局は上流からトークンを受信したときにこ れを取り込むことによって， 自局のデータを他局に発信する権利(発信権〉を 獲得する。IEEE8 0 2 . 5
規格[5J(以下，単に規格と呼ぶ〉は膨大な記述から成っ ているが，要約すれば各局は次のように動作することが想定されている。(1) どの局も発信権を確保していないとき， トークンはリング上を循環して
第7章 代数的手法のトークンリング方式LANへの応用 107 いる(図
7. 1
(a))。(2) 各局は，プロトコノレの上位層から渡された発信すべきデータ(プロトコ ルデータユニット
PDU
と略す〉を待ち行列内に保持しておく。待ち行列が空 でないときにトークンを受信すると，それを取り込むことによって発信権を獲 得した局(発信局〉となる。(3) 発信局は，発信に必要な制御情報(自局や着信局のアドレス等〉を待ち 行列中の各
PDU
に付加してフレームとし，一連のフレームをーっすやっ発信す る(図7. 1
(b))。(4) 発信権をもたない局(中継局)は，受信したフレームをそのまま下流へ 送信する。さらに，中継するフレームの着信局アドレスが自局のアドレスと一 致するとき，すなわち，そのフレームが自局宛のものであるときは，自局にそ
(a) J'4︑ LU )
recelver
(c) (d)
図7. 1 トークンリング方式 LANにおける発信権の割り当て
108 第7章 代数的手法のトークンリング方式LANへの応用
のフレームをコピーする(図
7. 1
(c))。(5) リング上を一周したフレームは，それを発信した局によってリングから 除去される。
(6) 発信局は一連のフレームの発信を終えると， トークンを発信することに より発信権を他局に譲り，中継局となる(図
7. 1
(d))。本章では，個々の入力パケットに対してどのような出力パケットを送信すれ ばよいかといった，局が行う個々の動作に着目するのではなく，より抽象的に，
その結果としての動作の履歴全体である入出力系列に着目する。どのような入 力系列にはどのような出力系列が送信されるべきであるかという，局の動作全 体を見た抽象度の高い，従って，局に課すべき要求の度合いの少ない仕様を代 数的に記述する。この仕様を満たす局が上述の意図通りに動作することを代数 的手法によって確かめ，二つの性質が成り立つことを検証する。まず，
7.2
で はプロトコルの代数的仕様を与える。この仕様は，プロトコルがもっと予想さ れる二つの性質，r
安全性J
(発信局から発信されたフレームは下流のある局ま でその内容を変更することなく伝達されるか，すべての局に伝達されるかのい ずれかであるという性質〉と「相互排他性J
(リング上でトークンは一つ，しか もただ一つしか存在しないとしづ性質〉が満たされるために必要な要求を記述 したものである。7.3
では，上記の性質が確かに成立することを形式的に証明 することについて述べる。なお，規格に盛られているフレームの発信に関する優先権等については，本 章では直接，記述や検証の対象としないので言及してはいない。一方，通信に は任意の長さの遅延が伴ってもよく，通信路には任意個のパケットが滞留して もよいとしている。この仮定は，遅延時間や通信バッファの大きさが有界であ るとすることによってもたらされる余分な記述を省いている。これらも仕様に 含めることはもちろん可能であり，その際には，本章の仕様に新しい公理等を 付け加え，必要に応じて一部を修正すればよい。
7.2 トークンリング方式 LANプロトコルの代数的仕様 規格として定められているトークンリング方式
LAN
の媒体アクセス制御プ第7章 代数的手法のトークンリング方式LANへの応用 109 ロトコルには，局の入出力動作が主に記述されている。本節では，そのうち，
安全性や相互排他性を検証するために必要な抽象度の高い仕様を，局の入力パ ケット系列 ISEQと出力パケット系列 OSEQとの聞に成立するべき関係とし て抽出することによって与える。 N個の局から成るトークンリング方式 LAN において，任意に選んだ局を局1として順次下流に向って局2，局3， …等と する。局nの代数的仕様を STATION(n)"，系全体の代数的仕様を RING
CN)"と呼ぶ。なお， これらの仕様は，代数的仕様記述言語ASL/M[6]を用い て書カ通れる。局が満たすべき性質やその検証に必要な記述も同様に ASL/M を用いて書かれる。
7 .2. 1
局の代数的仕様7 . 2 . 1 . 1
局における入力ノ〈ケット系列と出力パケット系列の対応の記述 各パケットは型と内容をもっ。パケットの型には， トークン 中間フレー ム"および 最終フレーム"の三つがある。発信局が発信する一連のフレーム のうち，最後のフレームが最終フレーム，そうでないフレームが中間フレーム である。局は， (1) 発信， (2) フレームの中継， (3) トークンの中継という三 つの基本動作を遂行する。(1) には， トークンの取り込み，一連のフレームの 発信，一巡してきたフレームの除去とトークンの開放が含まれる。三つの基本 動作それぞれが完結することによって次に示すような入力部分系列と出力部分 系列一対のパターン(以下，構成単位という〉が定まると考えてよい(図7.2( b ) ‑ ( d ) )
。系全体がその初期状態から出発して，これらの基本動作を繰り返したときの各局の ISEQおよび OSEQは，これらの基本単位を順次下から積み上 げた上に，基本動作(1)に対応する構成単位の初期部分系列をそれぞれ付加し たものである(図
7. 2
(a))。このような入出力系列に着目した局の仕様を表7 .
1に示す。構成単位の各対は，上述の局の基本動作に対応した次のパケット系 列である。
(1) 入力部分系列 AIA2…AkCk孟
2 )
において， Alがトークン， Akが最終 フレームであり，それ以外は中間フレームである。対応する出力部分系列 BIB2…
BmCm
孟2)
においてはBm
ー1が最終フレーム，Bm
がトークンであり，それ110 第7章 代数的手法のトークンリング方式LANへの応用
く二Component=
>
fO く=Component =
>
<
= Component士><
= Component =>
く=Component二>
fO