第 4 章 HDLC 手順の代数的記述
4.1
序 言プロトコルの正しさの検証のためには，まずプロトコル自身が厳密に記述さ れていなければならない。従来，プロトコルの記述法としては，状態を導入し 状態遷移図を利用する方法[2.5.10.12.13凶と，プログラミング言語を利用して記述 する方法[1.3.4.15]に，大別されてきた[9.1九前者の記述法は，単純ではあるが，
プロトコルを記述するのに要する状態数がその複雑化と共に指数的に増大し，
プロトコノレの本質的な構造を陽に表現するのが困難(例えば
8
の代りに6 4
を 法とした送受信順序番号を考えても，論理構造は不変であるにもかかわらず，その事実が適切に表現されなしうである。後者では，整数演算などを直接利用 できるのでこのような欠点を免れているが，記述に直接必要のないプログラム 要素の意味に依存し，利用するプログラム言語自体の意味の形式的定義が前提 となる。ところが，そのような定義自身一般にきわめて複雑である。さらに，
処理順序の一意的記述により過剰規定に陥り易いという欠点もある。
本章では，上記のような欠点を免れうる方法として 基底代数をもっ代数的 仕様記述法[日]を採用し，ハイレベルデータリンク制御
(HDLC)
手順の形式的 記述を示している。記述の前提となる基底代数としては，プール演算，整数の 加減算と大小判定など必要最小限に限り，手1I買に固有な概念はすべて陽に記述 している。まず，HDLC
手順の規格[8]を分析し，その基本的な概念を抽出し た。その結果に基づき， 4.2で示すように 1次局 2次局について，内部構 造を陽にもたない抽象的 状態"を導入し，基本動作に対応して 状態遷移関 数"を，また，状態から必要な情報を抽出するための 出力関数"を導入し，それらの聞に成立する関係を公理として表した。導入したデータタイプ(以下 ソートと呼ぶ)や関数はいずれも
HDLC
手順の規格の中に現れる概念に対応 するものであり，規格の記述からごく自然に関数聞の関係を簡潔に公理として44 第4章 HDLC手順の代数的記述
書き下すことができた。個々の公理が妥当であることは，規格における記述と の対応から容易にわかる。 4.3では，さらに公理系全体として 矛盾がなく"
かつ 不足なく"書かれていることを証明し，また，この公理系から
HDLC
手順を実現する 順序機械"を組織的に構成できることを示した。 4.4で、は，4.2
の1，2
次局に外部とのインタフェース部分を付加した1
，2
次局全体の 代数的記述を与えた。代数的仕様記述法の一つの利点は，記述が公理系として与えられているので，
ここで記述された手順で伝送が正しく行われているかとし、う検証は，検証すべ き命題がその公理系におけるいわゆる定理として成立するということを証明す ることである。従って，検証に関しでも，代数的記述の同じ枠組の中で議論で きる[6Jとし、う特徴をもっ。
4 . 2 HDLCの代数的記述
HDLC
規格のうち，不平衡型の基本手順クラスに関する部分の説明とその代 数的記述を示す。ただし，データリンクの設定，終結部分を除いた動作部分に 限定する。動作のモードはあらかじめ正規応答モードに設定されており，モード変換は行われないものとする。
4 . 2 . 1
フレームの代数的記述と諸定義HDLC
における送信単位をフレームと呼びその集合をframe
と書く。送信 順序番号と受信順序番号は整数0
，1，…7
を用い，その集合をseqnumber
で表す。ポールピット，ファイナルピットCPF
ピット〉をそれぞれ0， 1で 表し，PF
ピットの集合をp f
，また，情報部の集合をd a t a
で表す。このような各集合の 種類"
C
データタイプ")をソートと呼ぶ。送信順序番号，受信順 序番号，PF
ピット，情報部の四つの引数から情報形式フレームを構成する関数 をIframe
で，逆に，情報形式フレームからその成分である送信順序番号，受 信順序番号，PF
ピット，情報部を取り出す関数をそれぞれs s n
，r s n
，p f b i t
，i n f o r m
で表す。同様に，受信順序番号，PF
ピットの二つの引数からRR
C r e c e i v e r e a d y )
監視形式フレーム，RNR C r e c e i v e n o t r e a d y )
監視形式フ第4章 HDLC手順の代数的記述 45 レームを構成する関数を，それぞれ
RRframe
，RNRframe
で表し，逆に，そ れぞれの成分を取り出す関数をr s n
，p f b i t
(これらは上述のものと共通)で表 す。e r r o r f r a m e
はソートframe
の定数関数(ヲ￨数をもたない関数)である。一方，構成されたフレームが情報形式フレームか，
RR
監視形式フレームか，RNR
監視形式フレームか否かを判定する関数をt y p e I
，typeRR
，typeRNR
で 表す。さらに，フレームチェツクシーケンス(FCS)
による誤り検査で，誤りと判定されたとき真，そうでないとき偽となる関数
e r r o r c h e c k
がある。ここ での記述では，フレームに関して1
次局2
次局の記述に必要と考えられる 性質の記述に限定されており、情報形式フレーム，RR
監視形式フレーム，RNR
監視形式フレームをビット系列としてどのように表すかについては記述されて いない。すなわち，不必要な詳細は隠されている。また，ここのレベルでは，e r r o r c h e c k
(f)が真であるようなフレームはすべて同一視してよい。前述のe r r o r f r a m e
は，そのようなフレームを代表するものとして導入したものである (表4. 1
の公理AX21
参照〉。これらのソートや関数を用いてフレームの仕様 をASL/O
言語[l1Jで記述したものが表4.1
である。表
4.1
の表記法について，SPEC Framespec
;はこの仕様記述の名前がFramespec
であることを表し，BASE
…;により，ブールや非負整数やビット( 0
，1
だけの元を含む集合〉やデータ(+)に関するソートや基本演算がフレーム の仕様を記述する上で前提とされており(これを基底代数と呼ぶ)，改めて定義 することなく，それらを自由に用いてよいことを表す(このような仕様記述の 形式的な定義は文献C16 J
に与えられている)0SORT
…;は，記述の中で用い られるソートの名の宣言部であり，REL
…;でソート間の関係を規定してい る。例えばseqnumber
というソートはO
から7
までの非負整数であること を表している。OP
…;は関数のタイプを宣言する部分で，例えば， Iframe
seqnumber
，seqnumber
，d a t a
，pf‑
→frame
は，関数記号(以下単に関数 と書く)Iframe
の引数のソートがseqnumber
，seqnumber
，d a t a
，p f
で，関 (+) 単一ソート dataのオベレーションなしの任意の集合である。なお表4. 1中で大文 字で始まる DataやBoolなどは基底代数名を表し，小文字のdataやboolなどは それぞれの基底代数におけるソート名を表す。46 第4章 HDLC手順の代数的記述
表4. 1 フレームの代数的記述 SPEC Framespec ;
BASE Bool， NN‑integer， Bit， Data ; SORT frame， seqnumber， pf ;
REL seqnumber二 二 nn‑integer[0， 7J pf 二 二 bit;
OP Iframe : seqnumber， seqnumber， data， pf ‑> frame， RRframe， RNRframe : seqnumber， pf ‑> frame， typeI， typeR ，RtypeRNR : frame ‑> bool， ssn， rsn : frame
pfbit : frame inform : frame errorframe
一>seqnumber，
> pf， 一>data，
> frame， errorcheck : frame 一>bool ; V AR s， r SORT seqnumber，
d SORT data， b SORT pf;
AX 1: typeI(lframe(s， r， d， b))
==
TRUE;AX 2 : typeI(RRframe(r， b))
= =
FALSE;AX 3 : typeI(RNRframe(r， b))二 二 FALSE;
AX 4 : typeRR(Iframe(s， r， d， b))二 二 FALSE;
AX 5 : typeRR(RRframe(r， b))
= =
TRUE;AX 6 : typeRR(RNRframe(r， b))二 二 FALSE;
AX 7 : typeRNR(Iframe(s， r， d， b))二 二 FALSE;
AX 8 : typeRNR(RRframe(r， b))二 二 FALSE;
AX 9 : typeRNR(RNRframe(r， b))二 二 TRUE;
AX 10: ssn(Iframe(s， r， d， b))二 二 s， Ax 11: rsn(lframe(s， r， d， b))二 二 r;
AX 12: rsn (RRframe (r， b)) = = r ; AX 13: rsn(RNRframe(r， b)) = = r ; AX 14: pfbit (Iframe (s， r， d， b)) = = b ; AX 15: pfbit(RRframe(r， b)) = = b ; AX 16: pfbit(RNRframe(r， b)) = = b ; AX 17: inform (Iframe (s， r， d， b)) = = d ; AX 18: errorcheck(Iframe(s， r， d， b))二 二 FALSE;
AX 19: errorcheck(RRframe(r， b))二 二 FALSE;
AX 20: errorcheck(RNRframe(r， b))二 二 FALSE;
AX 21: errorcheck(errorframe)二 二 TRUE;
END;
第4章 HDLC手順の代数的記述 47 数値のソートが
frame
であることを表している。VAR
…;は各変数がどのソートに属するかを宣言する部分である。
AX1 ‑AX21
は，関数間の関係を公 理として書き下したものであり，公理の左辺はすべてフレームを構成する関数 の外側にそのフレームの各成分を取り出す関数をネストさせた形で書かれてい る。例えば，AX18
は，構成された情報形式フレームのFCS
による誤り検査 結果が偽であることを表している。4 . 2 . 2 1
次局と2
次局の代数的記述規格では，再送のためのデータの保持の仕方に関しては規定されておらず，
また， シンクやソースとのデータの授受， ラインへのフレームの送出 タ イマの起動，停止 など外部の環境に依存する部分やそれらの変化を引き起す 部分(し、わゆるインタフェース部分〉は， 自然語の意味に頼って唆昧にしか書 かれていない。まず，ここで記述の対象とするのは，規格で書かれていること から上述のデータの保持やインタフェース部分を除外した部分(図
4. 1
の1
次 局( P r i m a r y )
，2
次局( S e c o n d a r y )
であり，そこでは，動作はデータに依存 しないので，再送といった概念はない。その部分を整理，再編成したもの，お よび，それに対応する代数的記述を以下に述べる。なお，4.4
ではここで除外 した部分を含む規格全体について記述する。input ‑from ‑source output‑to‑sink ]IS primary
Line ~ ?hys!cal f Level (The data stream from secondary to primary is omitted)
図4. 1 プロトコルの階層構造
48 第4章 HDLC手順の代数的記述
( 1
，2
次局のソートと関数〕1
次局の抽象的な状態の集合をprimary
と書き，その初期状態を表す定数関 数をi n i t i a l
と書く。1
次局の基本動作として送信，受信，タイムアウトの3
種 類があり，これらの動作に伴し、1次局は状態変化を起す。これらの動作に対応 する関数として次の五つの関数が導入される。これらの関数は，動作を行う直 前の1
次局の状態 pおよび必要なパラメータを引数に含み，動作直後の1
次 局 の状態を関数値として与える。(1) 情報形式フレームを
PF
ピットb
で送信する関数:s e n d I ( p
，b
，) (2)RR
監視形式フレームをPF
ピットb
で送信する関数:sendRR ( p
，b )
， (3)RNR
監視形式フレームをPF
ピットb
で送信する関数:sendRNR ( p
，b )
， (4) フレーム fを受信する関数:r e c e i v e ( p
， f)，(5) タイムアウトを表す関数:
t i m e o u t ( p )
。ただし，これらの関数によって， どのようなデータが送受信されるか，ある いは，タイマが何時セットされ何時解除されるか，などに関しては，後の 4.4 の1次局全体の記述のところで述べられる。また，上記の基本動作がその状態 で許されない動作であるか否かを表す関数
i n v a
1id
を導入する。これは， ]IS
規 格で許されない動作の条件をひとまとめにして表す関数であり，初期状態から 許される動作のみを行ってきて到達した状態p
に対してi n v a
1id( p )
は偽であり，一度でも許されない動作を行っているとき真である。
さらに
1
次局の状態 pから，特定の情報を抽出するための関数をいくつか 導入する。s e q ( p )
は次に送信すべき情報形式フレームの送信順序番号を表す関 数。h i g h ( p )
は，最も最近にs e n dI ( p
，b )
により送信した新たなフレームの送 信 順 序 番 号 に8
を法として1
加 え た 値 を 表 す 関 数 で ， 再 送 の 際 に 対 象 と な る データの送信順序番号の上限を表す。a c k ( p )
は次に受信が期待される(2
次 局 からの〉フレームの送信順序番号の値を表す関数で，ack(p)‑1
の送信順序番 号までの情報形式フレームをすべて正しく受信したことを表し，a c k ( p )
の値 は送信順序番号として2
次局へ送られる。l o w ( p )
は(1
次局から2
次局への伝 送の)1
次局側で確認している2
次局側のack(
・〉の値を表す関数である。HDLC
手 順 に お け る 誤 り 回 復 の 基 本 手 順 は 1 ，2
次局間でのPF
ピット1"
第4章 HDLC手順の代数的記述 49 のフレームの順次交換により行われる。
1
次局が最も最近にPF
ピット1"
で送信したフレームの送信順序番号を表す関数を
c h e c k p o i n t ( p )
，既にPF
ピット1
"でフレームを送信したが，それに対する(2
次局からの)PF
ピット 1"のフレームが未受信であることを表す関数を
r e a d y ( p )
と書く。また，タイムアウト誤りを表す関数を
t ‑ e r r o r ( p )
，RNR
監視形式フレームを受信済 みで，それを解除する(2
次局からの〉フレームが未受信であることを表す関 数をb u s y ( p )
と書く。r e a d y
，t ‑ e r r o r
，b u s y
の各関数の値は，それに対応する 事象が起ったとき真，それを解除すべき事象が起ったとき偽となる。2
次局に関しては，その抽象的な状態の集合をs e c o n d a r y
と書く。正規応答 モードのとき2
次局は時間監視を行わないので関数t i m e o u t
やt ‑ e r r o r
はない。1
次局と2
次局の共通な部分の代数的記述を表4.2
に示す。表4.2
は，表4.
1の
Framespec
を部分仕様として含み(INCLUDE Framespec;
で宣言さ れている)， ソ一ト 、s t a t
旬e "
を/パξラメ一タとする仕様記述名がの代数的記述でで、ある。
1
次局と2
次局の代数的記述は，表4.2
のパラメータs t a t e
をそれぞれソートp r i m a r y
とs e c o n d a r y "
で置き換えたものを部分 仕様として含み，それに各局固有の関数と公理を付加したものとして表される (表4. 3
，表4.4)
。上述のソートや関数は，表4. 2‑
表4. 4
の中のSORT
部とOP
部でそれぞれ宣言されている。記述の略記法:表
4.2‑
表4.4
の公理において，左辺の下線は，その公理 の右辺の始めにI F N OT
(in v a l i d
(下線部))THEN
が省略されており，
THEN
以降の部分だけ書いていることを表す。この形より，
i n v a l i d
(下線部〉が真なら，下線部の 状態"に対するs e q
，h i g h
，…などの値は定義されていないことになる。〔基本動作の実行と状態変化〕
状態pにおいて，情報形式フレームを送信することができるのは，過去に許 されない動作を行ってなく(i